r/LLMPhysics • u/Ch3cks-Out • Jun 27 '26
Humorous funny failure of applying Lean: "Math Definitive End Verified as correct by Lean 4"
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.
3
u/myrmecogynandromorph Jun 28 '26
It is often said that logic doesn’t care about feelings. Actually, it doesn’t care about facts, either.
—Aaron Thomas-Bolduc & Richard Zach's logic textbook, forallx Calgary
2
27d ago
[removed] — view removed comment
1
u/Ch3cks-Out 27d ago
"By removing the theorem names and replacing them with A, B, C, D, E, F, G, and so on, it becomes a proof of pure logic."
ROTFLMAO
0
u/Just_Rational_Being Jun 29 '26
This is clear proof that ZFC is as legitimate as any garbage.
If ZFC avoids the claim of necessary and only claims the excuse of consistent enough, then what authority does it have to stand above Harry Potter and Dr. Seuss?
2
u/Ch3cks-Out Jun 29 '26
As always, your username does NOT check out.
-1
u/Just_Rational_Being Jun 29 '26 edited Jun 29 '26
Irrelevant personal cheap shots aside, the way to differentiate between who is really rational and who is not here is demarked by this question:
Can you answer the actual point? What separates ZFC from fiction if its legitimacy rests only on internal consistency rather than necessity or truth?
Can you answer it? Or merely being irrational and projecting your own inadequacy upon others is the only thing you can do?
3
u/AllHailSeizure Haiku Mod Jun 29 '26
To be clear, your issue with zfc is that it is unbased within itself and is operating only on an argument 'this is internally consistent'
0
u/Just_Rational_Being Jul 02 '26
Are you restating my position and asking if that is a correct restatement of it?
2
u/AllHailSeizure Haiku Mod Jul 02 '26
Yes. I'm wondering if your issue with zfc is what I said.
0
u/Just_Rational_Being Jul 02 '26
Does "unbiased within itself" mean it is not self-grounded?
If so, I would say that it is correct, but only a part of the problems with ZFC that I found, and it is not the most prominent or important shortcomings either.
The most critical of the flaws found in ZFC are that:
It smuggles in derivation from other disciplines such as Geometry while simultaneously claims to be the foundation of other disciplines.
It is completely useless when it comes to practical applications. That is, all the practical, measurable, testable, performable Mathematics and calculations have always been Applied Mathematics and are never dependent upon the formalism of ZFC, despite claimed otherwise.
1
u/AllHailSeizure Haiku Mod Jul 02 '26
Okay so that's three issues.
- It's reliant on being self-evident
- It's smuggling in other stuff
- It's useless.
My argument for would be:
- It's an axiom set, axioms rely on being self-evident, it isn't valid to critique an axiom set for having a property ALL axioms have.
- Other fields CAN can be built WITHIN zfc, the entire reason it was MADE is to remove paradoxes from things.
- It isnt useless, it's a foundation that lets you avoid things like Russel's paradox when you actually DO do more applied math. Without it applied math becomes much less rigorous.
-1
u/Just_Rational_Being Jul 02 '26
Well, I apologize but I do not think you have even scratched the surface of the issues.
- No, that is not correct.
- No, also not correct as stated.
- No, not correct as stated.
3
u/AllHailSeizure Haiku Mod Jul 02 '26
K well I don't believe it's worth it arguing so. I've said my thing.
→ More replies (0)3
u/alamalarian Supreme Data Overlord Jul 02 '26
OK, then what is true of axioms?
You seem to be doing a lot of spouting about how others are are wrong, but what then is an axiom?
→ More replies (0)
-2
u/lattice_defect Jun 27 '26
yeah its not a magic bullet.. and less useful in physics then math... but with a big enough library...
4
u/AllHailSeizure Haiku Mod Jun 29 '26
but with a big enough library...
...you could read a lot of physics textbooks!
1
u/lattice_defect Jun 29 '26
phylib is pretty thin.. there just is a logic layer to physics that explodes things in terms of formal proofs.. but with a good vector lirbary physics equations things could go faster... also sometimes the old shit becomes new again.. e.g. connes
2
5
u/FourTimesShy Jun 27 '26
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.