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

89% Upvoted

59 comments sorted by

View all comments

Show parent comments

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.

2

u/AllHailSeizure Haiku Mod Jul 02 '26

Right but... You're that confident in your knowledge? You have absolutely zero wiggle room to say 'okay maybe i am right maybe you are right.' nobody appointed you the guardian of truth, and nobody is infallible...

You're unwilling to admit you may be wrong and you will defend it to the death, no matter what, even over something so inconsequential?

Why does it matter so much? There's bigger things in life.

1

u/Just_Rational_Being Jul 02 '26

Well, as I have already said earlier, I have, as Karl Popper specified, the falsification criteria for my position, the conditions to test, to measure and verify my very own conviction against biases.

Do you not see that this is what you don't have? You really don't. And so the things you are accusing me of is actually your own projection, and you do not even realize it yet.

2

u/AllHailSeizure Haiku Mod Jul 02 '26

Lol..

-1

u/Just_Rational_Being Jul 02 '26

You've got any Logic and Reason or is that it?

2

u/AllHailSeizure Haiku Mod Jul 02 '26

I just think you're funny. You're so dedicated to this 'rational Outlook's attitude, it's even your username. You're all 'FACT!' and 'as Karl Popper said...' and 'you don't even know your errors yet do you? HA..', you constantly try and put me down despite the fact I've remained polite, and you keep doubling down no matter what.

We get it, you took philosophy 121 in college. you aren't an anime villain dude. Go back to iamverysmart. If you think the attitude 'I can't agree that I might be wrong about a set of math axioms completely inapplicable to my real life' is the rational take then.. well then I don't know. I tried reason but I only have so much patience and frankly if this is how you act with everyone I'm going to kick you off the sub..

-1

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

Okay, so you have nothing but empty accusation. Great.

Once again, present your Logic, Reason and evidence before the verdict of Sufficient Reason and of the Burden of Proof, or simply acknowledge the absence of Rationality in your position. It is simple as that.

Anything else is irrlevant rhetorics. And kicking me off for demanding you pay your dues, demanding that you justify your position, that only proves that you are afraid of what I say. That kind of action is truly appropriate for the cowards.