Does it work with Lean4?
The future of interactive theorem proving?
11–17 of 17 posts
Re: The future of interactive theorem proving?
#12This sounds like a cool demo, but I find it hard to imagine it being useful. For one, in order to check the output you need to be proficient enough that you might as well write the statement that you want. In addition, if you're working on a large library then there are small but important design decisions that matter for many statements, just like when designing ordinary software. I doubt that Codex is able to make…
I think one thing that this could help with is that, even if you are proficient in Lean, finding the way you are supposed to translate an informal statement into Lean/mathlib can be time-consuming if not a challenge -- it is a very large library, and it is mathematically heavy (being a library for theoretical mathematics). At the least, this gives you hints about which parts of mathlib you should be looking at.
Maybe! You're certainly correct that there's a difference between knowing Lean (or a given proof assistant) vs. knowing mathlib (or some specific library). It doesn't seem to me that Codex has much of an idea about the mathlib codebase, since it e.g. invented and used "tangent_space_at_identity" out of the blue. Library-specific training would improve on this, of course.
I would reach for the usual code search tools for getting familiar with a library. For example, in Coq you have the "Search" and "Print Hint" commands which let you search for terms and instances, respectively. I imagine Lean has something similar.
Re: The future of interactive theorem proving?
#13Earlier quoted context omitted.
I think one thing that this could help with is that, even if you are proficient in Lean, finding the way you are supposed to translate an informal statement into Lean/mathlib can be time-consuming if not a challenge -- it is a very large library, and it is mathematically heavy (being a library for theoretical mathematics). At the least, this gives you hints about which parts of mathlib you should be looking at.
Maybe! You're certainly correct that there's a difference between knowing Lean (or a given proof assistant) vs. knowing mathlib (or some specific library). It doesn't seem to me that Codex has much of an idea about the mathlib codebase, since it e.g. invented and used "tangent_space_at_identity" out of the blue. Library-specific training would improve on this, of course. I would reach for the usual code search tools…
> It doesn't seem to me that Codex has much of an idea about the mathlib codebase, since it e.g. invented and used "tangent_space_at_identity" out of the blue
But then perhaps it's a hint to the user that this API may be an useful abstraction, and perhaps one can use the same tool to define this function
Re: The future of interactive theorem proving?
#14While this is a very interesting exercise, I see this kind of wild optimism as when the compilers were introduced or "5th generation computer languages" or any other advance in that area, its touted as: "you can just tell the computer what you want in a simple, natural way, and it won't need programmers any longer" while any of those is a significatively improvement, it is very far from the dream.
>it is very far from the dream. SQL is the great success story of that generation. Writing database query and management code in an imperative language is a nightmare.
I don't completely agree.
Yes, SQL is a great success but no, the declarativeness was not enough and we end up generating SQL through ORMs, query builders, templating, etc
Re: The future of interactive theorem proving?
#15I want to preface this by saying I'm not trying to hate on the author. Good on them for applying a new technology to try to solve an annoying part of their work. I hope they continue to be creative and fearless in their approach to problem solving. The comments that follow are born more out of my increasing frustration with the ML and ML-adjacent communities that seem to have failed to learn anything about the danger…
(I'm the Johan Commelin mentioned in the blogpost.) In fact, `lie_group` exists in mathlib, and is defined as follows: /-- A Lie group is a group and a smooth manifold at the same time in which the multiplication and inverse operations are smooth. -/ -- See note [Design choices about smooth algebraic structures] @[ancestor has_smooth_mul, to_additive] class lie_group {𝕜 : Type*} [nontrivially_normed_field 𝕜] {H : T…
I figured there would be. It just provides another point that it's not really understanding, and it's not really "extracting the pattern".
I really wish half the effort on generation would be spent on leveraging them for guided exploration. It wouldn't matter if you were provided slightly incorrect suggestions for "likely relevant functions," but even likely correct source code doesn't cut it.
Or even snippet prototyping. Like don't use the generated text directly, provide an interface that I can use to transform the generated code into a snippet that I can save.
Re: The future of interactive theorem proving?
#16Earlier quoted context omitted.
>it is very far from the dream. SQL is the great success story of that generation. Writing database query and management code in an imperative language is a nightmare.
I don't completely agree. Yes, SQL is a great success but no, the declarativeness was not enough and we end up generating SQL through ORMs, query builders, templating, etc
I agree that there should have been more innovation on thosd aspects of query languages!
It's a little bit tricky because there aren't much low hanging fruits for academics to write good papers about, so this innovation is up to programmers who want to improve their quality of life when dealing with databases.
Re: The future of interactive theorem proving?
#17I want to preface this by saying I'm not trying to hate on the author. Good on them for applying a new technology to try to solve an annoying part of their work. I hope they continue to be creative and fearless in their approach to problem solving. The comments that follow are born more out of my increasing frustration with the ML and ML-adjacent communities that seem to have failed to learn anything about the danger…
It's a fair concern that ML model generates misleading definitions and statements which hides bugs and is hard to detect, but it also depends on how the user utilizes this kind of tools.
For any serious use case, before attempting to prove any statements, a responsible user should always carefully define any *top level statements* manually or hire a domain expert to write or review the definition.
Once we have high confidence on the definition of the top level statements, the user might start to break down the proving approach into a couple of auxiliary lemmas.
From this moment, they can freely play with machine generated code without too much safety concern, because:
* the ultimate goal is to prove the original top level statement, which is already human inspected;
* if the machine generates a misleading lemma, it won't help proving the top level statement, but it won't lead to a false claim as well, since the proof checker will reject any incomplete or incorrect proof.
The worst case is to be fooled by misleading lemmas and waste a lot of time exploring an unhelpful proof approach, which could be sad and costly but won't be a critical safety issue.
If ML assisted interactive theorem provers inspired by Lean Chat becomes productivity tools, users should be educated to always do their best to ensure the top level statement is exactly what they want to define, this should be an industry common practice. For critical usage, a theorem prover UI can even enforce this practice by disable auto code generation for top level statements.