Hacker News Reader

Comment by i_no_can_eat | Hacker News Reader

Can you elaborate on what constitutes a vacuous proof?

> Can you elaborate on what constitutes a vacuous proof?

Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.

When I first started playing with lean I accidentally defined a group in such a way that it was reduced to triviality. It had one object in it, so everything in the group was trivially equal to everything else. It was not the group that I was trying to prove something about, but the proof went through.

It was too easy, so I double checked my definitions, but it is quite easy to do something like that. And Claude does things like that quite frequently.

I am going through the exercise right now of trying to get Claude to formalize a published paper and it is a _struggle_ to get it not to take shortcuts or prove approximations of the paper’s theorems and then tell you it’s done.

It can happen when the proof process ends up with universal implication that holds trivially. Then you end it with something like Forall x, x is empty -> P(x).

I present to you my new theorem as follows:

If 1 == 3 then 3 == 3

----

This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.

For a laymen, I don't follow this.

Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?

> How is it logically coherent?

It's not. But Lean doesn't interrogate logical coherence, just internal consistency.

No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.

“if X then Y” means “(not X) or Y”

E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet.

This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.)

Many hard problems are answered this way.

For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture.

Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians.

But if your precondition is “stupid,” your proof is stupid.

if A then B

Can only be false if there is an instance where A is true, and B is false. In all other cases it's true, even when A is always false.

That's the key.

It is just the definition of "Logical Implication for Material Conditional" and its truth table; see Material Conditional - https://en.wikipedia.org/wiki/Material_conditional

I highly recommend the following two books to study Logic from the beginning (for a layman);

Logic: An Introduction to Elementary Logic by Wilfrid Hodges.

Introduction to Logic: and to the Methodology of Deductive Sciences by Alfred Tarski.

Nothing to do with special hacks with operators. The reason it's useless because the precondition is never true. "If my aunt had two wheels and a handlebar then she'd be a bicycle" Is the same problem with a non maths flavour.

This is known as a “vacuously true” statement in formal logic. Let me write it out more in more detail and you’ll hopefully see why it’s consistent.

In logic, a proposition is some statement that can be true or false. So, let A be the proposition that 1 equals 3, and B be the proposition that 3 equals 3.

Now the poster is making a third proposition. If A, then B.

A is clearly not true. So in classical logic, B can be anything and “If A then B” is still true.

For example let B be the proposition that I am Elvis Presley (I’m not). So now we have “If one equals 3 then I am Elvis Presley”. This is clearly true. I’m not Elvis Presley, but that doesn’t matter because we’re not saying anything about what happens when one doesn’t equal 3.

Now, let’s try let B be the proposition that I am Sean Hunter (I actually am). So now we have “If one equals 3 then I am Sean Hunter”. This is clearly still true because we still are only making a claim about what happens when one equals three.

https://en.wikipedia.org/wiki/Vacuous_truth

By the way, this isn’t any kind of inherent contradiction or problem, it is just a possibly counterintuitive part of how classical logic works.

You see this type of statement (“If <x>, then <something ridiculous>”) being made a lot when people are exaggerating for effect, for example by Mr Bumble in “Oliver Twist”

   > 'That is no excuse,' replied Mr. Brownlow. 'You were present on the occasion of the destruction of these trinkets, and indeed are the more guilty of the two, in the eye of the law; for the law supposes that your wife acts under your direction.' … 'If the law supposes that,' said Mr. Bumble, squeezing his hat emphatically in both hands, 'the law is a ass--a idiot. If that's the eye of the law, the law is a bachelor’

https://www.literaturepage.com/read/olivertwist-460.html

If you have a software engineering background, it's like how semantic versioning is bollocks.

Semantic versioning describes the following idealized setup:

- you have an interface you expose (a contract, and thus a contract signature)

- you do not change the contract signature -> patch version bump

- you do change it but in a non-breaking way (e.g. additively) -> minor version bump

- you do change it but in a breaking way (e.g. mutatively or destructively) -> major version bump

One would expect then that since interface signatures are statically derivable, semantic version tags can be auto-assigned. And indeed, in lots of shops that's exactly what happens (in my opinion, correctly).

The problem with this is that it comes with a lot more smoke than fire. The interface having no changes or non-breaking changes doesn't mean the actual code behind those interfaces is not going to cause a breakage. It literally is just about the interface itself.

And so unless you encode absolutely everything about the semantics your implementation actually observes into the interface, which is what the semver specification asks you to do so as their sleight of hand, this means the interface will be a leaky abstraction. Which means that external software interfacing with yours may observe behavior that is beyond the purview of semantic versioning. Which means that they do. Which means that they absolutely can and will break, and your package managers' fancy version constraint syntax exists to make such fun events happen.

The way this is usually handled then is:

- you live with the pain: acknowledge the limitations of semver, accept you've been duped, and just give in

- you have human release managers assign versions manually, based on whole program and whole system semantics (with the human overhead and error that entails), falsely claiming that what you're doing is still semver

- you switch to a less deceptive versioning scheme, like calendar versioning; as a bonus, you now no longer have to pretend that your entire application somehow only has a single unified interface

This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface. The way the proof is derived may expose semantic gaps in the statement itself, and (ab)use them to obtain the logical consistency certificate. Hence, a vacuous proof, and hence why this is not statically assertable to be not the case. It is part of the challenge in asserting that the statement was correctly formalized in the first place: you need to manually identify whether the way the consistency was achieved is actually meaningful, or just a formalization gap.

Which really makes me wonder about the actual value proposition of Lean then, but alas...

  > This mirrors the Lean statement and Lean proof situation. The statement is like an interface, and the proof is like the implementation behind that interface.

This is true in a very deep sense due to the Curry-Howard correspondence and calculus of constructions which are central to Lean. In Lean, the proposition you are proving is a type (so it really is an interface directly in the computer science sense) and the proof is a function which takes your hypotheses and returns a term of that type (so it really is the implementation of that interface). In fact in lean, you can just as well write this implementation as a lambda (this is known as “term mode”) as in the “tactic mode” that is more generally used in normal lean use. Lean really doesn’t care at all which one you use and you can switch between them within a proof quite easily without interfering with lean’s ability to check your proof at all.

   > Which really makes me wonder about the actual value proposition of Lean then, but alas...

The purpose of lean really is quite different from what most people on hn seem to want it to be. Lean is designed to be a useful tool for mathematicians who want to formalise areas of mathematics. It’s not a primary goal of most of the lean community to make something that is hardened against malicious proof attempts (although these are considered bugs and there is a small subcommunity who work on this area in particular). So it isn’t primarily for the benefit of people who want to “fire and forget” some proof without reading or understanding it and just get the check mark if it’s true.[1] It’s mainly for mathematicians who want a proof assistant to help them with their work.

[1] there are sub-tools such as comparator that are designed for this type of use case. https://github.com/leanprover/comparator

Reply on news.ycombinator.com