Proof Explorer
Mathematical ideas and proofs created with AI. Explore what checks in Lean and what remains open.
Recent actual results
A polynomial counterexample to weak Markus–Yamabe in dimension eightAn explicit polynomial map with Jacobian spectrum −1 everywhere and three distinct rational zeros. Read the paper and its complete Lean certificate.
Projects
- Riemann Hypothesis
Every non-trivial zero of ζ lies on the critical line
- P vs NP
Can every efficiently verifiable problem be solved efficiently?
- Irrationality of √2
Fermat descent, from naturals to the reals
- Jacobian discovery lab
Four results: Hurwitz dimension eight, exact image, middle-branch rigidity, Gaussian moduli