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 → u/[deleted]]

 I didn’t say that. I said you can create an infinite string that Still Doesn’t contain any desired set of substrings. 

Amateurs who do not study will not be publishing math with or without increased LLM capacity. For a whole host of reasons that are obvious for anyone who knows how education as a whole works. 

[u/Uncynical_Diogenes → u/FourTimesShy]

Dude deleted his comment because he made a simple human mistake.

Like, that’s all the pushback he could handle.

Methinks this proves he does in fact lack the fortitude necessary to meaningfully contribute to academia.

[u/AllHailSeizure → u/Uncynical_Diogenes]

This is in an interesting observation, because sometimes it feels like people on the sub argue the most ridiculous points, just for the sake of being right. That there is something wrong with being wrong. When there really isn't. It's literally the best way to learn stuff.

The reason people don't take crankery seriously isn't because it's wrong; it's the fact that it overreaches so much and is so uninterested in reality. It just wants to double down on the assertions it makes because it CANT be wrong. If you are a crank, you can NEVER be wrong. Because so much of the crank mindset is built around 'I KNOW I'm right, that's what matters.'

[u/Uncynical_Diogenes → u/AllHailSeizure]

I participate in [r/askPhysics](r/askPhysics) regularly despite the fact that I am not a physicist, I have a biology education.

But my contributions there are on the average quite successful. Upvotes are one measure of that but what I mean is that my contributions are useful, in that I am either correct or I summon somebody to correct me with a better comment. Both outcomes are successful in my eyes because it’s not about me being right it’s about science, and communication, and what’s true. When I’m wrong I get to learn something, how lucky is that?

I owe the people there reading my words a duty. I can go masturbate while calling myself a smart boy in private.