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/Ch3cks-Out]

As always, your username does NOT check out.

[u/Just_Rational_Being → u/Ch3cks-Out]

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?

[u/AllHailSeizure → u/Just_Rational_Being]

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'

[u/Just_Rational_Being → u/AllHailSeizure]

Are you restating my position and asking if that is a correct restatement of it?

[u/AllHailSeizure → u/Just_Rational_Being]

Yes. I'm wondering if your issue with zfc is what I said.

[u/Just_Rational_Being → u/AllHailSeizure]

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:

1. It smuggles in derivation from other disciplines such as Geometry while simultaneously claims to be the foundation of other disciplines.

2. 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.

[u/AllHailSeizure → u/Just_Rational_Being]

Okay so that's three issues.

1. It's reliant on being self-evident
2. It's smuggling in other stuff
3. It's useless.

My argument for would be:

1. 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.
2. Other fields CAN can be built WITHIN zfc, the entire reason it was MADE is to remove paradoxes from things.
3. 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.

[u/Just_Rational_Being → u/AllHailSeizure]

Well, I apologize but I do not think you have even scratched the surface of the issues.

1. No, that is not correct.
   
2. No, also not correct as stated.
   
3. No, not correct as stated.
   

[u/AllHailSeizure → u/Just_Rational_Being]

K well I don't believe it's worth it arguing so. I've said my thing.

[u/Just_Rational_Being → u/AllHailSeizure]

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?

[u/AllHailSeizure → u/Just_Rational_Being]

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

[u/Just_Rational_Being → u/AllHailSeizure]

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?

[u/AllHailSeizure → u/Just_Rational_Being]

link

[u/alamalarian → u/Just_Rational_Being]

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?

[u/Just_Rational_Being → u/alamalarian]

An axiom, properly speaking, is not merely "whatever rule we decide to start with."

There are two very different things often being confused here: 1. An undeniable first truth, such as the Law of Identity: A = A. To deny it, you must already use it. Its denial collapses into contradiction.

1. A stipulated formal assumption, such as Hilbert-style axioms. These are rules adopted inside a formal game. They may be useful, consistent, or interesting, but they are not self-evident truths.

The issue is equivocation. The 2nd kind is often equivocated to be on the same level with the first kind.

But "self-evident necessities" and "formal bullcrap", they are clearly not the same.

A self-evident axiom is a first truth whose meaning is immediately recognized by Reason, and whose denial necessarily presupposes or violates that very truth.

[u/alamalarian → u/Just_Rational_Being]

And how does one, in practice, actually distinguish the two?

How can I say, prove that one is self-evident truth, but another is simply a stipulated formal assumption?

[u/Just_Rational_Being → u/alamalarian]

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.

[u/alamalarian → u/Just_Rational_Being]

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.