2
$\begingroup$

Would it be possible to only write declarations and conclusions and write a program that automatically fill in theorems used to derive those conclusions in LEAN 4? From my understanding, proof assistants like LEAN 4 ask users to fill in theorems, elaborate, and then type-check. Please forgive me in case my question is too vague. I am new to proof assistants.

Edit: Thanks Jason Rute for his detailed answer. After reading his answer, I realize I should specify "fill in theorems provided each conclusion could be derived by applying one theorem from a library". Could such a hammer like program be written and would it be practical to use such a program to write proofs?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ This is called "proof automation". Proof Assistants do do this to some degree, with the help of hammers, for example. But this is basically a research question. As such, there is no "push-button" theorem prover that can tackle any proof $\endgroup$ Commented Aug 24, 2024 at 1:51
  • $\begingroup$ I don’t understand your updated question. You want the proof to just be an application of a theorem already in the library? If so, Lean has a tactic exact? which checks if your current goal is just a direct application of a theorem already in the library. Is this what you are looking for? $\endgroup$ Commented Aug 24, 2024 at 13:19
  • $\begingroup$ @JasonRute Thanks for taking the time. I know the 'exact' tactic fill in a known theorem. But I am looking for a program (or opinion on whether it's possible to write one) that, when given all proved statements and all theorems in the library, choose a subset of the proved statements and a theorem with matching input and output. So, more like 'aesop' than 'exact'. $\endgroup$ Commented Aug 24, 2024 at 13:30
  • $\begingroup$ @JasonRute The GitHub page of 'aesop' says 'you tag a (large) collection of definitions with the @[aesop] attribute, registering them as Aesop rules.' Could theorems be tagged as Aesop rules? $\endgroup$ Commented Aug 24, 2024 at 13:49
  • 1
    $\begingroup$ I’m referring to exact? (with a question mark at the end, it used to be called library_search), not exact. $\endgroup$ Commented Aug 24, 2024 at 17:14

1 Answer 1

Reset to default
5
$\begingroup$

Most proof assistants build proofs with tactics. Tactics are commands that help build the proof for you. Some tactics are very low-level like intros or apply, while other tactics are designed for doing much more powerful logical or mathematical manipulations.

There are a number of tactics that are designed to fill in whole proofs. Some ones that work in special cases are:

  • reflexivity (for definitionally equal proofs)
  • simp (for proofs which follow from rewriting the expressions in a standard way)
  • ring (in MathLib, for proofs about integers and other rings)
  • linarith (in Mathlib, for proofs about linear arithmetic)

There are also the following general automation tools which are for completing arbitrary proofs:

  • aesop (in Mathlib, can also be used as its own package Aesop)
  • duper (currently in development, does first-order reasoning and I think much more, will probably be pretty powerful)

Even more powerful are (or will be) tactics or other tools that call out to other powerful tools. One such type of tactic is called a hammer. Hammers call out to external (first-order logic) solvers. The Isabelle proof assistant has a really powerful hammer called SledgeHammer. Lean is building its own hammer:

The other direction is to use modern AI. There are a lot of works in this field. See the recent A Survey on Deep Learning for Theorem Proving. But even since that survey, there have been three fairly powerful projects.

  • AlphaProof by DeepMind. It took three days but it can solve 3 of the recent IMO problems. (And its sister project AlphaGeometry solved the geometry problem.) It represents the state of the art, but isn't practical right now since it requires a lot of computation and is specifically trained for IMO problems.
  • DeepSeek-Prover v1.5 Also very powerful, and open source, but again it is trained to solve competition-style problems, and it likely requires a lot of computation to get the results in the paper.
  • InternLM2-StepProver Also open source and powerful. I don't know as much about this one.

The main problem with the state-of-the-art works is that they are research projects. There hasn't been as much work on practical tools yet. The two I know right now that you can run on your Laptop are:

Also, some people have found generic general-purpose code assistants helpful like ChatGPT, Github Copilot, Tab9, or other LLM coding assistants (some of which are free). Your mileage may vary.

Also see the recent Lean Zulip post AI/ML tools for Lean.

The general idea seems to be that the current tools–especially the neural AI tools, but also the symbolic ones–are getting better and better. But we haven't spent as much time turning these projects into something practical that you can run either on your Laptop or via a free/cheap API.

Of course, not all theorems can be filled in automatically. For example, asking an AI to solve the Riemann Hypothesis is yet a bit out of reach. :) (And after that, it would violate several logical theorems to have an AI that could always fill in any provable theorem automatically.)

Where we are at now depends on your use case and how many resources you are willing to put toward this.

  • Current tools can fill in relatively simple proofs of special cases.
  • Upcoming tools could do even more of the "obvious" stuff for us, including searching the library for theorems you need.
  • Current state-of-the-art ideas could be used to fill in harder proofs but it would take time and computation since they involve search algorithms (albeit, quite smart ones) which take time to work. Good use cases would let the algorithms run overnight, or even for a week, possibly on some external server to fill in missing proofs. We may even be able to use such a system to solve some (relatively easy) open problems.
  • Better tools would both allow us to do more for the user in real-time and also solve more powerful proofs with long time scales.
  • As the technology grows we might invest more time in just letting the systems run and solve new proofs or do whole chores like formalizing a complete paper, but we aren't there yet. One problem is that we don't have systems yet that can do the long-term planning and organization needed for such tasks. (I don't know how soon we will have such systems.)
Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ Nice answer. It might be worth remarking that what the OP is asking for is impossible, as there is no general algorithm that decides whether a theorem has a proof, by a theorem of Alan Turing's. So all these tactics and neural networks, they "just" do the best they can. $\endgroup$ Commented Aug 24, 2024 at 23:27

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.