I have no background in math, so this might be naive, but 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?
IIUC you're saying that basically someone with a mental database should be able to identify preconditions matching some theorem and postconditions aligned with the next statement from their mental database.
Or is there math that can't be expressed in a way for proof checkers to assess atm?
Edit: Or maybe proof checker use just isn't as wide-spread as I imagined. It sounds like the state statically typed languages in programming...
> 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.
IIUC you're saying that basically someone with a mental database should be able to identify preconditions matching some theorem and postconditions aligned with the next statement from their mental database.
Or is there math that can't be expressed in a way for proof checkers to assess atm?
Edit: Or maybe proof checker use just isn't as wide-spread as I imagined. It sounds like the state statically typed languages in programming...