One place for every development in AI and mathematics.
AI will prove results that mathematicians then need to understand. We digest those proofs, step by step and from first principles. We also use AI for better progress in mathematics, and we study the mathematics behind AI itself.
AI mathematics for a better and humane world.
The film above: Meet AI Mathematician, 54 seconds. Music: “Floating Cities” by Kevin MacLeod (incompetech.com), licensed under CC BY 4.0. Download it in 4K, with the logo and banners, from the brand kit.
AI proves. We digest.
A machine-found proof is only the start. A digest rebuilds it for a human reader: every prerequisite, every computation, every idea, in order, until the result is understood and not merely checked.
Keller asked in 1939 whether a polynomial map with constant nonzero Jacobian determinant must have a polynomial inverse. In 2026 a counterexample in three variables was found with AI (pending peer review). Its determinant is exactly −2, yet three points share one image.
Over 50 detailed videos digest it from polynomials and determinants up to the counterexample itself. More volumes are upcoming.
The common language behind proof, prediction, and design.
Mathematics has two complementary roles. In pure mathematics, claims are developed structurally: definitions, lemmas, theorems, and proofs derive new knowledge from first principles. In the sciences, hypotheses are written mathematically and then tested against observation, experiment, simulation, and engineered behavior.
Both roles matter for future AI. A system that can reason with formal structure can help verify proof steps. A system that can connect mathematical models with data can help formulate better simulations, optimization problems, and scientific hypotheses.
From mathematical prose to machine-checked proof.
Lean and mathlib turn mathematical statements into executable objects. Definitions become precise, proofs become checkable, and the verifier confirms whether every inference follows from accepted foundations and imported results.
State the object
Translate the claim into a typed formal statement with explicit assumptions.
Build the proof
Use definitions, lemmas, tactics, and library results to construct the argument.
Verify the result
Lean checks the proof term and rejects gaps, type errors, or unsupported steps.
A concrete theorem, written for a verifier.
The proof below is intentionally simple. It shows the core pattern: a mathematical statement is expressed in Lean syntax, and Lean validates that the proof really establishes the statement.
import Mathlib
theorem pythagorean_triple :
3 ^ 2 + 4 ^ 2 = 5 ^ 2 := by
norm_numVerified
Lean checks the statement, expands the numerals and powers, and accepts the proof only when the normalized arithmetic establishes the equality. If the proof term is wrong, the theorem does not compile.
Proof and observation reinforce different kinds of truth.
Self-contained mathematics
Definitions and axioms support long chains of deductive reasoning. Formal systems let AI tools search, fill, refactor, and verify those chains with much tighter feedback than informal prose alone.
Mathematics for nature
Physics, chemistry, biology, engineering, and simulation express hypotheses in equations, operators, constraints, and objectives. These models are validated by measurement, prediction, and real-world performance.
Machine learning as a new modeling layer
Neural networks often solve useful problems without exposing first principles the way a conservation law or partial differential equation does. The frontier is to connect learned behavior with mathematical structure, explanation, and verification.
Let's develop mathematics together.
Whether it's formalization consulting, a research collaboration, or training for your team — get in touch.