Prompt Engineering for Mathematics
Mathematics is one of the most interesting frontiers for LLMs: the outputs are verifiable, the benchmarks are hard, and working mathematicians are publicly folding these tools into their research workflow. Formal proof assistants and language models are starting to collaborate in earnest.
Where this is showing up in Mathematics
- DeepMind's AlphaProof and AlphaGeometry 2 reached silver-medal-level performance at IMO 2024 — the first AI system to earn any Olympiad medal, published as "Olympiad-level formal mathematical reasoning with reinforcement learning" (Nature, 2025).
- AlphaProof is trained with reinforcement learning to generate formal proofs in Lean 4 against the mathlib library, using test-time RL to adapt to each problem.
- Terence Tao has publicly documented formalizing proofs in Lean 4 with GitHub Copilot and the
canonicaltactic — including a ~33-minute formalization of a Bruno Le Floch proof from the Equational Theories Project. - Tools like LeanCopilot (lean-dojo) embed LLM-based tactic suggestion and premise selection directly inside Lean, making proof automation practical for undergraduate coursework.
Projects you could build in this course
- A Lean proof-assistant copilot that helps a student formalize a textbook theorem
- A problem-set tutor that checks each step with a CAS or symbolic verifier
- A theorem-to-English translator that explains a mathlib proof in plain language