What Would Leibniz Say About AI Mathematics?

Discovery Versus Verification

The emergence of advanced mathematical reasoning in Large Language Models (LLMs) raises a fundamental question:

Is mathematics essentially logical deduction, or is it a creative activity in which logic serves primarily to verify discoveries?

Some 350 years ago Gottfried Wilhelm Leibniz (1646–1716) distinguished between two mathematical activities:

Ars inveniendi — the art of discovery.

Ars judicandi — the art of judgment or verification.

Leibniz wanted to mechanize both. His characteristica universalis was intended as a universal symbolic language, while his calculus ratiocinator would transform reasoning into calculation.

His famous invitation was Calculemus! — Let us calculate!

The Unexpected Route of AI

For centuries, automated mathematical reasoning was pursued through formal logic, from Boole and Frege to Turing and automated theorem proving.

Modern AI has taken a different route.

LLMs were initially trained to predict the next word or token in human language. Yet from this training emerged capabilities for mathematical reasoning, problem-solving and even mathematical discovery.

Why?

Because human language already contains logical structure: implications, negations, quantifiers, analogies and chains of reasoning.

By learning language, including mathematical texts and computer programs, AI acquires reasoning capabilities without being explicitly programmed as a conventional theorem prover.

Mathematical reasoning has emerged, in an important sense, as a byproduct of language modeling.

Discovery Is Not Verification

Formal logic determines whether a conclusion follows from given assumptions. But it does not determine which assumptions to make, which questions to ask or which discoveries are meaningful.

Mathematical creation involves analogy, imagination, experimentation and computation. Logical deduction establishes the validity of proposed conclusions.

Language generates possibilities. Logic tests necessities.

Leibniz might ask: Why should discovery itself not be computational?

Modern AI suggests that it can be, without being reduced to explicitly programmed logical deduction.

Thus two computational activities emerge:

Generative AI → Mathematical Discovery

Formal Logic → Mathematical Verification

Both are computational, but only the second provides a guarantee of logical validity when correctly implemented.

Mathematics Creating Mathematics

The historical irony is remarkable:

Mathematics → Computation → Language Models → Mathematical Reasoning → New Mathematics → Improved Computation → ...

Mathematics has created a computational instrument capable of contributing to its own further development.

Leibniz sought to construct a language for logical reasoning. AI has acquired mathematical reasoning capabilities by learning from existing human language.

Leibniz sought to put logic into language. AI has extracted mathematical reasoning from language.

Perhaps mathematics is not primarily a formal logical enterprise, but a creative, language-like activity whose results can be logically verified.

Leibniz's Calculemus! thus acquires a new meaning:

Let us calculate—not only to establish what is true, but to discover what might be true.