> Source URL: /math.guide
---
title: "Prompt Engineering for Mathematics"
description: "How LLMs and proof assistants are changing mathematical research — and what you could build with them in this course."
---

[@styles]: ./styles.css

# 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"](https://www.nature.com/articles/s41586-025-09833-y) (*Nature*, 2025).
- **AlphaProof** is trained with reinforcement learning to generate formal proofs in **[Lean 4](https://lean-lang.org)** against the **[mathlib](https://leanprover-community.github.io)** 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 `canonical` tactic — including a ~33-minute formalization of a Bruno Le Floch proof from the [Equational Theories Project](https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/).
- Tools like **[LeanCopilot](https://github.com/lean-dojo/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

[← Back to Thinking With Machines](./index.path.md)


---

## Backlinks

The following sources link to this document:

- [Mathematics](/index.path.llm.md)