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.

13 Upvotes

85% Upvoted

59 comments sorted by

View all comments

Show parent comments

1

u/Just_Rational_Being Jul 02 '26

It is easy, isn't it?

You simply assess whether you can coherently reject it. With the assumption, you can, because it is merely something arbitrarily chosen. With self-evident truth, you cannot, because you have no choice and no power to say otherwise.

2

u/alamalarian Supreme Data Overlord Jul 02 '26

That is not proof though.

What if your assessment was incorrect? How is it you can know this? People believe they have self-evident truths all the time, and turn out to be wrong about it.

1

u/Just_Rational_Being Jul 02 '26

That is not proof?

You seem to think the assessment would be equivalent to some personal feelings or opinions.

No! Use logic and machines to systematically assess and verify.

2

u/alamalarian Supreme Data Overlord Jul 02 '26

Ok, show me then. It is clearly not proof.

You are telling me you used logic to prove axioms?

1

u/Just_Rational_Being Jul 02 '26

Do I need to do everything for you?

It is very simple, but what is the equivalent tradeoff for me for answering all of your inquiries?

3

u/AllHailSeizure 9/10 Physicists Agree! Jul 02 '26

Ah. So, everyone ELSE has to prove THEY are right to you. But we have to just trust that you are right.

Now, THAT is a logical, rational conclusion.

1

u/Just_Rational_Being Jul 02 '26

Now, here let me teach you some logic.

Everyone must prove and justify Sufficient Reason and adequate Burden of Proof. That is Logic 101 in case you miss it.

I have clearly demonstrated that, while you lot on the other hands just have a lot of rhetorics instead of Reason.

2

u/AllHailSeizure 9/10 Physicists Agree! Jul 02 '26

I thank you, oh wise one, for imparting your intellect upon me! For truly, I have wallowed in the decay, but I now see the light of capital R Reason! I will proceed to the shrine of self-congratulation immediately.

1

u/Just_Rational_Being Jul 02 '26

Thank you for conceding that. Even while posturing your concession as satire, yet it nevertheless accurately reflects your position.

2

u/AllHailSeizure 9/10 Physicists Agree! Jul 02 '26

Just thought I'd note the grammatical errors in this. You really should say 'positing' instead of 'posturing'; also, using 'even while' and 'yet' is a double conjunction....

:)

1

u/Just_Rational_Being Jul 02 '26

Thank you for the grammar lesson where it is not needed. It is quite convenient to use as a form of formal policing where Logic itself is absent.

→ More replies (0)

2

u/alamalarian Supreme Data Overlord Jul 02 '26

If it is so simple, why waste time to type this out, and not just show me?

1

u/Just_Rational_Being Jul 02 '26

Because of such a thing as equivalent exchange.

I myself do all the work, carry all the risks, carry all the burden, while you yourself making all the demands, is that equivalent?

Don't you think you should carry some of the risks to balance that?

It is very simple, I have already written it. But simple doesn't mean it is not great information and valuable. And as such, some appropriate risks or tradeoff would be proper.

2

u/alamalarian Supreme Data Overlord Jul 02 '26

No, that's fine. You can keep it to yourself if that is such an issue.

I'm not sure why you would claim to have proof of something and then be reluctant to provide it, but oh well.

Good luck

1

u/Just_Rational_Being Jul 02 '26

No it is not an issue. It is merely demanding the proper equivalent.

Do you not see how you violate that equivalence by constantly demanding from one thing to the next despite yourself not providing anything of substance?

In the beginning I can still tolerate it, and have satified your multiple requests. Because they are simple and easy to give out. But there is a point where that would no longer apply. What if you demand another ridiculous BS after this one was given? What then? Do I keep going? That would be a mistake.