Hacker News Reader

Comment by chr15m | Hacker News Reader

> Autumn of verified Lean kernels

Above my pay grade, but it sounds like some kind of super cool self-hosted recursive lean-checker-in-lean.

I notice there are a bunch of caveats in that part of the article. If you were an LLM strongly RL'ed to give humans the result they're asking for, using recursion bugs to satisfy the goal would probably be something you would try.

I'm by no means an expert but I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.

View on HN

What do you mean by a "recursion bug"? The terminology does not occur in the article so it seems to be a term that means something to you that is not very clear to me.

I am conflating (probably ignorantly) the idea in software development of bugs in recursive code, with the potential for bugs when using Lean to check Lean’s checker.

> I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.

You are just making glib statements without having the necessary background. Hence it is difficult for people to engage with you since we have no idea whether what we say is understandable by you. I suggest that you go through some of the resources mentioned here (and other similar HN threads) to get some necessary background after which we all can have a better informative discussion.

How do you think Mathematicians were accepting each other's proofs before computers came along? They used a process like;

1) Relying on the prover's honesty (i.e. he is not intentionally trying to deceive).

2) Providing a mandatory proof idea (i.e. the main outline) for clear communication and comprehension.

3) Clear definitions/assumptions/statements of the problem/theorem to be proved.

4) Rigorous application of a few small logical reasoning steps viz. Deductive/Inductive reasoning, Logical Operations (specifically Implication/Converse/Inverse/Contrapositive), Rules of Inference, Quantifiers and basic structural conversions.

5) Walking through and validating the given proof by multiple mathematicians and ensuring that the results match. The Lean kernel can be considered as another prover in the peer-review group.

All of the above (and more) are already being followed by the mathematical community w.r.t Lean (and other proof assistants).

The drudgery of mechanically applying logical rules (point 4 above) is pushed onto the Lean kernel which is trusted, while the Human can concentrate on semantic correctness viz. problem/theorem definitions/assumptions/statements and the initial axioms. That is why the tool is called a "proof assistant".

Some important resources (focus on the concepts in the context of logical reasoning and not simply on the syntax);

1) Did you prove it? - https://leanprover-community.github.io/did_you_prove_it.html

2) Validating a Lean Proof - https://lean-lang.org/doc/reference/latest/ValidatingProofs/

3) Is there a way to guarantee that Lean 4 proofs cannot be adversarially tricked? - https://proofassistants.stackexchange.com/questions/6517/is-...

> without having the necessary background... it is difficult for people to engage with you since we have no idea whether what we say is understandable by you.

That must be frustrating. Thank you for trying and engaging with me anyway.

Those links were very informative, thanks for sharing!

It seems like there are a lot of things to worry about (even more than I realized after reading the main article) when using a proof assistant to try and figure out what is true. As they point out in the material you linked to, this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.

From what you've said and linked to it seems like you agree with the thrust of my original comment, or are you just saying "mathematicians already realize all of this you idiot," in which case I accept the charge!

I don't think endorsing scepticism and epistemic humility is a glib statement. These are fundamental mental tools when trying to figure out what is true.

> mathematicians already realize all of this

This is what i mean. Mathematicians and even more so Logicians (philosophers included) understand this and have the checks-and-balances in place when it comes to verifying and validating proofs and automated theorem provers.

> this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.

No; The resources i provided already detail how this problem is solved eg. using different independent proof checkers and comparators outside the Lean kernel.

If needed, You can also do re-verification using other completely different proof assistants (eg. Rocq etc.), using different LLMs and finally by a Human.

Lean itself operates under a zero-trust architecture and doesn't care about who the prover is, whether Human or LLM. So the LLM can generate anything (good/bad/hallucinations/whatever) but it all needs to pass as a proper proof term in the checker following the defined rules of inference which is what is enforced by the small and verified kernel. Think of Lean as providing a "strict compiler for mathematical logic".

Hence the reason i said you need to have some background in mathematical logic used in Proofs and how they are mapped onto Lean syntax.

The point i am making is that you are asking very fundamental questions more to do with the Philosophy of Logic which are already known and solutions/workarounds devised and implemented by both Humans and in Proof Assistants.

Reply on news.ycombinator.com