Learners formalize aspects of Peano arithmetic in a tutorial for this programming language called The Natural Number Game. For 10 points each:
[10h] Name this language whose Mathlib library contains “tactics” used for computer formalization in mathematics. Like Agda and Rocq (“rock”), this language is dependently typed.
ANSWER: Lean [accept Lean 3 or Lean 4]
[10m] In May 2025, Terence Tao released a Lean repository to complement his textbook on this mathematical subfield, which rigorously introduces calculus concepts like continuity and convergence using “epsilon-delta” definitions.
ANSWER: real analysis [accept Analysis I; reject “complex analysis”]
[10e] Kevin Buzzard leads an ongoing project to formalize this theorem in Lean using a refinement of Andrew Wiles’s original approach. This theorem states there are no positive integer solutions to “a-to-the-n plus b-to-the-n equals c-to-the-n” for n greater than two.
ANSWER: Fermat’s last theorem [prompt on FLT; reject “Fermat’s little theorem”]
<Editors, Other Science>