practal (u/practal) - Readit News

practal commented on From Zero to QED: An informal introduction to formality with Lean 4 sdiehl.github.io/zero-to-... · Posted by u/rwosync

lgas · 4 days ago

> Personally, I don't think that is much of a problem, as you should be able to come up with a "superlean" version of your theorem prover where correctness is easier to see, and then let the original prover export a proof that the superlean prover can check.

I think this is sort of how lean itself already works. It has a minimal trusted kernel that everything is forced through. Only the kernel has to be verified.

practal · 4 days ago

In principle, this is how these systems work. In practice, there are usually plenty of things that make it difficult to say for sure if you have a proof of something.

practal commented on From Zero to QED: An informal introduction to formality with Lean 4 sdiehl.github.io/zero-to-... · Posted by u/rwosync

mutkach · 5 days ago

I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.

practal · 4 days ago

You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I want to write it down in Practal [2], this becoming possible I see as the first serious milestone for Practal. Eventually, I want Practal to feel more natural than paper, and definitely more natural than LaTeX. That's the goal, and I feel many people now see that this will be possible with AI within the next decade.

[1] http://abstractionlogic.com

[2] https://practal.com

practal commented on From Zero to QED: An informal introduction to formality with Lean 4 sdiehl.github.io/zero-to-... · Posted by u/rwosync

mutkach · 5 days ago

Understanding IMO is "developing a correct mental model of a concept". Some heuristics of correctness:

Feynman: "What I cannot build. I do not understand"

Einstein: "If you can't explain it to a six year old, you don't understand it yourself"

Of course none of this changes anything around the machine generated proofs. The point of the proof is to communicate ideas; formalization and verification is simply a certificate showing that those ideas are worth checking out.

practal · 5 days ago

Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this.

Formalisation and (formulating) ideas are not separate things, they are both mathematics. In particular, it is not that one should live in Lean, and the other one in blueprints.

Formalisation and verification are not simply certificates. For example, what language are you using for the formalisation? That influences how you can express your ideas formally. The more beautiful your language, the more the formal counter part can look like the original informal idea. This capability might actually be a way to define what it means for a language to be beautiful, together with simplicity.

practal commented on From Zero to QED: An informal introduction to formality with Lean 4 sdiehl.github.io/zero-to-... · Posted by u/rwosync

lgas · 5 days ago

I'm not sure I understand what you're getting at -- your last paragraph suggestions that you understand the point of formal specification languages and theorem provers (ie. for the automated prover to verify the proof such that you just have to trust the toolchain) but in your next to last paragraph you speak as if you think that human mathematicians need to verify the lean 4 code of the proof? It doesn't matter how many lines the proof is, a proof can only be constructed in lean if it's correct. (Well, assuming it's free of escape hatches like `sorry`).

practal · 5 days ago

> Well, assuming it's free of escape hatches like `sorry`

There are bugs in theorem provers, which means there might be "sorries", maybe even malicious ones (depending on what is at stake), that are not that easy to detect. Personally, I don't think that is much of a problem, as you should be able to come up with a "superlean" version of your theorem prover where correctness is easier to see, and then let the original prover export a proof that the superlean prover can check.

I think more of a concern is that mathematicians might not "understand" the proof anymore that the machine generated. This concern is not about the fact that the proof might be wrong although checked, but that the proof is correct, but cannot be "understood" by humans. I don't think that is too much of a concern either, as we can surely design the machine in a way that the generated proofs are modular, building up beautiful theories on their own.

A final concern might be that what gets lost is that humans understand what "understanding" means. I think that is the biggest concern, and I see it all the time when formalisation is discussed here on HN. Many here think that understanding is simply being able to follow the rules, and that rules are an arbitrary game. That is simply not true. Obviously not, because think about it, what does it mean to "correctly follow the rules"?

I think the way to address this final concern (and maybe the other concerns as well) is to put beauty at the heart of our theorem provers. We need beautiful proofs, written in a beautiful language, checked and created by a beautiful machine.

practal commented on Why Fei-Fei Li and Yann LeCun are both betting on "world models" entropytown.com/articles/... · Posted by u/signa11

nmaley · a month ago

LLMs are parameter based representations of linguistic representations of the world. Relative to robot predictive control problems, they are low dimensional and static. They are batch trained using supervised learning and are not designed to manage real time shifts in the external world or the reward space. They work because they operate in abstract, rule governed spaces like language and mathematics. They are ill suited to predictive control tasks. They are the IBM 360s of AI. Even so, they are astonishing achievements.

LeCun is right to say that continuous self supervised (hierarchical) learning is the next frontier, and that means we need world models. I'm not sure that JEPA is the right tool to get us past that frontier, but at the moment there are not a lot of alternatives on the table.

practal · a month ago

See, I don't get why people say that the world is somehow more complex than the world of mathematics. I think that is because people don't really understand what mathematics is. A computer game for example is pure mathematics, minus the players, but the players can also be modelled just by their observed digital inputs / outputs.

So the world of mathematics is really the only world model we need. If we can build a self-supervised entity for that world, we can also deal with the real world.

Now, you may have an argument by saying that the "real" world is simpler and more constrained than the mathematical world, and therefore if we focus on what we can do in the real world, we might make progress quicker. That argument I might buy.

practal commented on Why don't you use dependent types? lawrencecpaulson.github.i... · Posted by u/baruchel

zozbot234 · 2 months ago

How does the proof of correctness work in this case? Is the rewriting ultimately resorting to proof steps within the kernel like a LCF-tactic would, or is there simply an informal argument that whatever you're doing in the rewriter is correct, on par with the proof kernel itself?

practal · 2 months ago

There is a proof as part of my thesis that the engine is correct, but it is not formal in the sense of machine-checked.

Note that the final result of the Flyspeck project does not depend on that proof, as the linear inequalities part has later on been redone and extended in HOL-Light by Alexey Solovyev, using just the LCF kernel of HOL-Light. Which proves that using a simple LCF kernel can definitely be fast enough for such computations, even on that scale!

practal commented on Why don't you use dependent types? lawrencecpaulson.github.i... · Posted by u/baruchel

stevan · 2 months ago

> That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.

I don't think it's "basically the same", because this application of the rewrite rules in a LCF-like system is explicit (i.e. the proof checking work grows with the size of the problem), while in proof by reflection in a type theory it happens implicitly because the "rewriting" happens as part of reduction and makes use of with the definitional equality of the system?

For small and medium examples this probably doesn't matter, but I would think that for something like the four colour theorem it would.

practal · 2 months ago

As I said, it depends on how you practically implement it.

I've used it for proving linear inequalities as part of the Flyspeck project (formal proof of the Kepler conjecture), and there I implemented my own rewrite engine for taking a set of rewrite rules and do the computation outside of the LCF kernel, for example by compiling the rules to Standard ML. You can view that engine as an extension of the LCF kernel, just one more rule of how to get theorems. In that instance, it is exactly the same.

practal commented on The new calculus of AI-based coding blog.joemag.dev/2025/10/t... · Posted by u/todsacerdoti

svieira · 2 months ago

No, a proof proves what it proves. It does not prove what the designer of the proof intended it to prove unless the intention and the proof align. Proving that is outside of the realm of software.

practal · 2 months ago

Yes, indeed, a proof proves what it proves.

You confuse spec and proof.

practal commented on Why don't you use dependent types? lawrencecpaulson.github.i... · Posted by u/baruchel

stevan · 2 months ago

> Proof by reflection is accomplished by running some arbitrary program during proof checking that has been proven to only return a "true" result if the goal is true. You can do the exact same thing in an LCF system, and in fact that's arguably what a complex LCF "tactic" amounts to in the first place.

I think the difference is that in a type theory you can prove the soundness of the decision procedure to be correct within the system?

From "Metatheory and Reflection in Theorem Proving: A Survey and Critique" by John Harrison, 1995:

> "No work on reflection has actually been done in HOL, but Slind (1992) has made some interesting proposals. His approach is distinguished from those considered previously in two important respects. First, he focuses on proving properties of programs written in Standard ML using the formal semantics to be found in Milner, Tofte, and Harper (1990). This contrasts with the other approaches we have examined, where the final jump from an abstract function inside the logic to a concrete implementation in a serious programming language which appears to correspond to it is a glaring leap of faith. [...]"

Proving that your LCF-like tactics are sounds using the (informal) semantics of the tactic language (ML) seems cumbersome.

Furthermore I believe proof by reflection crucially relies on computation happening at the logical level in order to minimise proof checking. Harrison concludes:

> "Nevertheless it is not clear that reflection’s practical utility has yet been convincingly demonstrated."

This was from 1995, so fair enough, but Paulson should be aware of Gonthier's work, which makes me wonder if anything changed since then?

practal · 2 months ago

The basic idea is: You run a program F on some input x, obtain r, and then you have some sort of justification why F x = r is a theorem. There are various levels of how you can do this, one is for example that "running the program" consists of applying a curated set of (proven) rewriting rules that take you from the theorem F x = F x to the theorem F x = r by applying them only to the right hand side. That is basically the same as "Proof by reflection" as used by Gonthier, where the Coq kernel acts as the (unverified) rewriting engine.

So this is not a matter of dependent or static typing or not, the idea is simple and the same (e.g., I've used it for my PhD thesis in Isabelle that is from 2008), it is just a matter of how practical this is to use in your theorem prover of choice.

practal commented on The new calculus of AI-based coding blog.joemag.dev/2025/10/t... · Posted by u/todsacerdoti

AstralStorm · 2 months ago

Don't worry, you're going to be searching for logic vs requirements mismatches instead if the thing provides proofs.

That means, you have to understand if it is even proving the properties you require for the software to work.

It's very easy to write a proof akin to a test that does not test anything useful...

practal · 2 months ago

No, that misunderstands what a proof is. It is very easy to write a SPEC that does not specify anything useful. A proof does exactly what it is supposed to do.