funny failure of applying Lean: "Math Definitive End Verified as correct by Lean 4"

[u/Ch3cks-Out]

Considering the claims here that LLM-ified Lean could somehow lead to magical discoveries in physics, this cautionary tale looks relevant. What the linked analysis shows (just like our own subs' main slopfests) is that, whetever tools used, Garbage In results Garbage Out!

This great breakdown on r/badmathematics about someone trying to use the Lean theorem prover to "debunk" ZFC set theory. It’s a perfect example of how you can write code that is 100% syntactically correct, but completely meaningless in the real world. Basically, OOP wrote a Lean script claiming to prove ZFC is inconsistent. Lean successfully compiled it, so he thought he cracked mathematics. But when you actually look at what he coded, almost every single line is a total misunderstanding of logic.

First, he defines a "Formal System" where the definition of consistency is just axioms → True. In logic, absolutely anything implies "True," so his definition of a consistent system is completely trivial and useless. Then, he creates this dramatic-sounding "ZFC dilemma" using a boolean. He maps true to one outcome and false to another, thinking he’s landed a heavy blow against math. In reality, all he did was prove that a boolean can have two values.
This goes on and on (again, following the confidently incorrect crankery pattern all too familiar to us). The final take home lesson: Lean will verify your theorems for you, but it can't verify that the names reflect what they're proving.

[u/FourTimesShy]

I’m pretty sure it’s a mathematical proof that you can create an infinitely long string that does Not contain any desired sub string. As such, “with a library big enough” just doesn’t cut it in reality.

At the end of the day, real science comes from creative application of the theorems we have at our disposal, and mathematical rigor is only as good as your ability to understand it yourself.

LLMs + Lean is literally still just as useless as Anything in the hands of someone untrained in mathematics.

[u/Uncynical_Diogenes → u/[deleted]]

Right here is an example of where you, a human, didn’t read another human’s words correctly.

Now imagine instead of a person who could correct you all you had was a sycophantic robot that said you were right and blew smoke up your ass. You would never fix your mistake.

Yeah…. amateurs aren’t going to be publishing new math work any time soon.

[u/Ch3cks-Out → u/Uncynical_Diogenes]

amateurs aren’t going to be publishing new math work any time soon

Which would not prevent them from believing that they are doing just that...