Is there a decent overview of what the aim of mathematics solvers is these days? In light of Hilbert's effort at formalism in the 1920s, and the incompleteness theorem, I was wondering where this was going, and what the known limitations are.
The incompleteness theorem isn’t an argument against formalism, it’s just a bound on what you can do with it (you can’t use one set of axioms and expect to prove everything). That’s ok, because you are,
1. Not required to prove everything which is true,
2. Not limited to one set of axioms.
The nice thing about formalism is that you can use a computer program to check whether a proof is sound or not. Isn’t that nice? It has applications in e.g. computer science and engineering, where you can prove that a program does not crash, or prove that a traffic light never shows green in conflicting directions, or prove that a real-time kernel always provides enough computational time for your rocket computer to steer.
Working math, there are more and more complex proofs that cannot reasonably be checked by humans. Having a computer check them is a nice alternative.
Current hopes (even by Terrence Tao) are that you give a sketch of a proof to GPT-X and it will give you a link to the formally confirmed proof.
Others hope that the next AI will come up with a sketch of a proof itself.
GPT-4 sucks at lean because lean had it's syntax changed too often, and GPT-4 shows limited reasoning capabilities
However it did come up with the following proof for my little order of pairs
instance LT : LT (ℕ × ℕ) where
lt f g := f.1 < g.1 ∨ (f.1 = g.1 ∧ f.2 < g.2)
instance : DecidableRel (LT.lt : ℕ × ℕ → ℕ × ℕ → Prop) :=
fun (a,b) (c,d) =>
if h₁ : a < c then isTrue (Or.inl h₁)
else if h₂ : a = c then
if h₃ : b < d then
isTrue (Or.inr ⟨h₂, h₃⟩)
-- the rest is even more silly since we have to turn everything around
else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) =>
Or.elim h
(λ hlt : a < c => absurd hlt h₁)
(λ heq : a = c ∧ b < d =>
absurd (And.right heq) h₃))
else isFalse (λ (h : a < c ∨ (a = c ∧ b < d)) =>
Or.elim h
(λ hlt : a < c => absurd hlt h₁)
(λ heq : a = c ∧ b < d =>
absurd (And.left heq) h₂)
)
This may lead back to the original question because Bool ≠ Prop and the formula for LT should ideally lead directly to decidability without all this redundancy?
