71–73 of 73 posts
Earlier quoted context omitted.
That's a bad analogy. LEAN is a leading bleeding edge proof verification tool.
Fortran used to be the only programming language (and even cutting edge by default). People went off and created new ones anyway.
Earlier quoted context omitted.
(Sorry for the long post, but yours brought me thinking about a bunch of different aspects.) First of all, I did not mean to downplay elegance at all. I agree that elegance is very important and that math is very much about trying to find elegant ways to think about various problems and phenomena. It also makes math feel more human and art-like, as elegance is not completely objective. And I also agree that LLMs do n…
> I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems. If you were using Isabelle/HOL, then (depending on field) you could already have had this. Sledgehammer is pretty powerful, even though it's "just"¹ SAT solvers plus (not-quite-naïve) brute-force. Writes awful proofs (even i…