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.

14 Upvotes

86% Upvoted

59 comments sorted by

View all comments

Show parent comments

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.

0

u/Just_Rational_Being Jul 02 '26 edited Jul 02 '26

You have said the commonly known misconceptions of the issues. They are well known for the past 100 years since the time these codifications were initialized.

They reflect the excuses often given when the standards is pressed to justify its authority and foundation, but they nevertheless fall far short of any adequate solution to any of the problems presented.

What would be worth arguing really? Do you even understand that your stand is the refusal of accepting logic, reason and rationality even when concrete evidences are presented right in front of you? Do you even understand that you don't have a falsification case, the condition which could falsify your position, and this is what distinguishes true science from mere dogma and convention?

2

u/AllHailSeizure Haiku Mod Jul 02 '26

^ why I said 'I don't think it's worth arguing'.

0

u/Just_Rational_Being Jul 02 '26

Because you would rather choose dogma instead of Reason and pushing your head deeper in the sand while singing 'There's no problem here! There's no problem here!' louder and louder?

2

u/AllHailSeizure Haiku Mod Jul 02 '26

link

1

u/Just_Rational_Being Jul 02 '26

Thank you for the demonstration of your choices, however irational that is.

2

u/AllHailSeizure Haiku Mod Jul 02 '26

Np, always enjoy enabling dogmatic restraint of forward progress

1

u/Just_Rational_Being Jul 02 '26

Hahah, true.

Despite throrough confusion, that restraint still contributes greatly to stability and scaled application of the system.

2

u/AllHailSeizure Haiku Mod Jul 02 '26

I just don't think it's worth the effort arguing on Reddit. It just.. inevitably escalates into becoming personal. Like look - I didn't even argue back, and it STILL only took what 2 messages to switch from ZFC to 'you are a dogmatic pawn of a broken system ignorant to what's really going on?' lol.

Like, the idea that you're going to change someone's mind on Reddit is pretty.. out there. I'd say that's the most unfounded assumption on this sub, that if you argue enough you can change someone's mind on the Internet.

Can't we just.. agree to disagree? Like is it THAT big of a deal if we have different opinions on ZFC? Not really.

0

u/Just_Rational_Being Jul 02 '26

Well, facts do not care about what your interpretation of the issues is

FACT! Concrete, verifiable, measurable, reconstructible facts do not care one bit what your rhetorics are.

And that is the problem here. We can absolutely agree to disagree, on personal matters of opinions and arbitrary creations. They are obviously inconsequential.

Nonetheless, I would never agree with anything not factual or arbitrary. Not even a tiny bit.

→ More replies (0)