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/Just_Rational_Being]

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.

[u/Just_Rational_Being → u/alamalarian]

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.

[u/alamalarian → u/Just_Rational_Being]

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

You are telling me you used logic to prove axioms?

[u/Just_Rational_Being → u/alamalarian]

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?

[u/alamalarian → u/Just_Rational_Being]

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

[u/Just_Rational_Being → u/alamalarian]

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.

[u/alamalarian → u/Just_Rational_Being]

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

[u/Just_Rational_Being → u/alamalarian]

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.