Learn to Lean in 3 Steps
An experiment formalizing ten papers in Lean from end to end (and the caveats mathematicians should understand before trying it themselves).
-
-
Dawn or Twilight? Mathematicians in the LLM Era
What AI's mathematical breakthroughs may mean for mathematicians, and why the future depends on automation, connection, and adaptation.
-
Prompting Toward a Conjecture
How one sentence about searching the literature changed GPT-5.6 Sol Ultra’s success rate on Feige’s 1/e conjecture.
-
LLMs for Proof Generation and Verification
How GPT-5.5 Pro generated a proof resolving the binary-matrix case of a 1997 conjecture—and why pairing LLM proof generation with Lean verification may become a common mathematical workflow.