> shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps?

> shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps? This is essentially exactly what Mathlib[1] is, which is Lean's database of mathematics, and which large portions of the FLT project will likely continually contribute into. [1]: https://github.com/leanprover-community/mathlib4/ https://github.com/leanprover-community/mathlib4/ (Other theorem provers have similar libraries, e.g. Coq's is called math-comp: https://math-comp.github.io/ https://math-comp.github.io/ )