Posted by jlebar 15 hours ago
Now they have the perfect stress test to hill-climb and optimize.
This is not even a new proof, or at least they don't claim that it is. It's the formalization (in Lean) of an existing proof. That means, they are 'porting' the proof to a theorem proving programming language.
Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter
/s
This was initially "completed" in the 80s. You can see the timeline for cleaning up the proof in e.g. this mathoverflow answer
https://mathoverflow.net/questions/114943/where-are-the-seco...
it's something that some people have been waiting decades for, and is not yet completed.
No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.
https://lean-lang.org/doc/reference/latest/Axioms/#standard-...
The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α
The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b
The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)