future of proof assistant tools

Stream: general

[Arthur Paulino]

Truly generic question from an outsider who just started studying the field of proof assistant tools:
How do you see this field evolving? Where are we going?

[Scott Morrison]

It's a big question!

[Scott Morrison]

A few near-term (small number of years) plausible milestones:

• transition to a proof assistant language that is both expressive for mathematics, and fast for computation/tactics (Lean4)
• achieve fairly complete coverage of material taught in (pure) mathematics courses in a good bachelors degree, and substantial coverage of masters level material
• an increasing number of "headline" projects, involving collaborations between non-proof-assistant-aware mathematicians, proof-assistant-aware mathematicians, and computer scientists (e.g. Liquid Tensor Experiment)
• once we have Lean4, substantial improvements to automation, so the boring stuff gets easier
• ML based tools (for proof generation, premise selection, theorem search) integrated in the basic tooling, and used everyday
• once we have Lean4, parallel development of programming libraries, so the underlying language can also be used for general purpose programming

And aspirationally:

• PhD students in good math departments routinely knowing how to use a proof assistant (as a few generations ago happened with TeX :-)
• it not being unusual for research papers in pure mathematics to include partial or complete formalisations
• offering the lure of provable correctness in an ergonomic programming language to the rest of the world.

[Jason Rute]

I think there are a lot of possibilities of using AI (whatever you think AI is) to:

• find proofs (similar to current hammer systems, except it will output a readable proof)
• search theorem proving libraries
• and advise users on next steps in their proofs

There are even other AI possibilities which are more cutting edge:

• assist in all aspects of writing Lean code (see Open AI codex for inspiration)
• provide a black box choice tool for tactics (see Daniel Selsam and team's work)
• automatically translate between theorem proving libraries
• automatically filling in missing small lemmas in a theorem proving library
• fill in proofs for theorem statements alone for regular sized theorems (imagine an AI agent automatically filling in proofs for formal abstracts, or a small team focusing on the outline of a theorem proving project while an AI which is running in the background 24/7 is slowly over weeks filling in the proofs).

Even more crazy, but not at all impossible:

• AI agents which formalize latex papers
• AI agents which automatically find theorems in arXiv and match them to their formalizations in various libraries
• AI agents which automatically explore mathematics and build up non-trivial (at least for computers) knowledge
• AI agents which help you formally (or informally) prove theorems

[Jason Rute]

I also think @Mario Carneiro's MetaMath Zero is a cool project which opens up many possibilities, like:

• Having a kernel which can check any theorem prover's logic (Lean, Coq, Mizar, etc) and therefore give a secondary guarantee that an ITP library is sound (with respect to it's logic---it doesn't necessarily prove that the logic is consistent, although that is possible too).
• Having that kernel (not only the code, but the compiled machine instructions) (self-)verified, in the sense that it is verified to follows its checking instructions.
• Having a really fast way to store and check compiled proofs.
• Having a simple, fast, and easy-to-use interchange format for proof assistants, which at the least allows any proof in one theorem prover to be checked with another theorem prover (modulo some additional axioms).
• This interchange format could in theory allow communication of formalizations between ITPs, allowing one ITPs work to be usable in another. (Note, even though this is very possible in theory, it will be a pain to align definitions between theorem provers at scale. I think this is an area where AI could really provide value.)

[Arthur Paulino]

Amazing answers, thanks everyone.
Do we have a (big) library of proofs written in Lean? I'm asking this due to @Scott Morrison's second point:

achieve fairly complete coverage of material taught in (pure) mathematics courses in a good bachelors degree, and substantial coverage of masters level material

[Scott Morrison]

Oh! Yes. :-) We are a very substantial way towards this goal already. Meet mathlib.

[Scott Morrison]

https://leanprover-community.github.io/mathlib_docs/ is the main documentation page

[Arthur Paulino]

So much going on :D

[Arthur Paulino]

What do you think is the biggest barrier that prevents people from getting into this world?

[Yury G. Kudryashov]

Here is what comes to my mind:

• most of graduate level math is nor formalized yet;
• you can't say "apply thm A from paper B with trivial modifications", especially if "trivial modifications" are not trivial;
• new language, new technology;
• prejudice.

[Scott Morrison]

Yury G. Kudryashov said:

• you can't say "apply thm A from paper B with trivial modifications", especially if "trivial modifications" are not trivial;

Relatedly, as you get into using a theorem prover I can promise lots of frustrating moments when the theorem prover says "no: that's a square peg you're trying to put in a round hole", and you'll know it "morally" fits but have to do some work before the computer gets it.

This is something where there is huge scope for more helpful tactics (and why not throw in some ML!), but we have a long way to go.

[Apurva Nakade]

Let me use this awesome question to rant a bit.

In many cases, the level of generalization currently in Mathlib makes it completely unreadable and unusable for me, and possibly for many others. Here for example is the fundamental theorem of calculus.

[Apurva Nakade]

I think mathlib has really lost sight of readability and usability by non-expert mathematicians.

[Scott Morrison]

There are two (independent?) directions of expertise at play here: Lean and mathematics. Saying that generalization is a problem (completely valid) is more an issue for non-mathematics-experts, rather than non-Lean-experts.

[Scott Morrison]

There are excellent reasons for proving theorems in great generality. But your complaint is a good one --- it's hard to get your teeth into mathlib as a result. What should we do?

[Scott Morrison]

More tutorials would obviously help --- ideally linked to from module-docs (and even doc-strings on "famous" theorems).

[Scott Morrison]

We've largely avoided writing specializations of big theorems for purely pedagogical reasons (but we do write them when its convenient, and in special cases you can fill in some arguments from others).

[Scott Morrison]

We almost entirely avoid writing examples in mathlib. This is something I'd personally prefer to do a bit differently. As an example, perhaps we could have an example immediately below the statement of the FTC that @Apurva Nakade linked, just stating the easiest special case, with its proof just a call to the general version.

[Yury G. Kudryashov]

@Apurva Nakade Could you please provide more information? If we're talking about the next theorem in the file, which parts of the statement make it unreadable for you?

[Yury G. Kudryashov]

I understand why this version is hard to read but without the docs#interval_integral.FTC_filter trick we would need many more theorems to cover all left/right cases.

[Apurva Nakade]

I absolutely understand the need for generalization and I'm not saying that we shouldn't prove things in full generality. But it is too much assume that someone who wants to use the FTC should also know about Banach spaces and Filters when this is something taught in the first semester of college.

Here's the statement of the same theorem from Isabelle/HOL:

theorem fundamental_theorem_of_calculus:
  fixes f :: "real ⇒ 'a::banach"
  assumes "a ≤ b"
      and vecd: "⋀x. x ∈ {a..b} ⟹ (f has_vector_derivative f' x) (at x within {a..b})"
  shows "(f' has_integral (f b - f a)) {a..b}"
  unfolding has_integral_factor_content box_real[symmetric]

Even though I don't know any Isabelle/HOL I know immediately that this is the standard fundamental theorem and I can use it as a blackbox.

[Apurva Nakade]

I'll have to think more about suggestions ...

One that comes to mind immediately is just having a core library with the most generalized theorems and then just having an auxiliary one with specializations, like the most trivial form of FTC statement that a first year undergraduate can understand (it's not really a part of "undergraduate curriculum" if you need to know graduate level math to understand it :-/)

[Apurva Nakade]

If I remember correctly, mathlib also no longer has definition of a vector space. Which again is totally understandable as it is redundant and a module over a field is the same thing. But now how to explain rank-nulity theorem to someone who hasn't taken a course on ring theory?

[Apurva Nakade]

Scott Morrison said:

We almost entirely avoid writing examples in mathlib. This is something I'd personally prefer to do a bit differently. As an example, perhaps we could have an example immediately below the statement of the FTC that Apurva Nakade linked, just stating the easiest special case, with its proof just a call to the general version.

This would be a great idea.

[Apurva Nakade]

I just want to clarify that I'm not saying that I know a better way to do things. I understand that a lot of thought and work goes into each definition, theorem and proof. But nevertheless the end result is that theorems are no longer recognizable in their "textbook formats".

[Apurva Nakade]

(Actually, this might mostly be true for analysis because of the use of filters and stuff at the very start.)

[Mario Carneiro]

Apurva Nakade said:

I absolutely understand the need for generalization and I'm not saying that we shouldn't prove things in full generality. But it is too much assume that someone who wants to use the FTC should also know about Banach spaces and Filters when this is something taught in the first semester of college.

Here's the statement of the same theorem from Isabelle/HOL:

theorem fundamental_theorem_of_calculus:
  fixes f :: "real ⇒ 'a::banach"
  assumes "a ≤ b"
      and vecd: "⋀x. x ∈ {a..b} ⟹ (f has_vector_derivative f' x) (at x within {a..b})"
  shows "(f' has_integral (f b - f a)) {a..b}"
  unfolding has_integral_factor_content box_real[symmetric]

Even though I don't know any Isabelle/HOL I know immediately that this is the standard fundamental theorem and I can use it as a blackbox.

This is an unusual complaint, considering that the Isabelle/HOL statement explicitly uses both banach spaces (you can see it in the type of f) and filters (has_vector_derivative takes a filter, and at x within {a..b} is a filter). Is the issue then that the notation is better? Because it seems to be stated at about the same level of generality.

[Johan Commelin]

This might also partly be due to the verbosity of the docs (they include all the namespaces and such).
I find the actual source more readable than our web docs:

/-- Fundamental theorem of calculus-1: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
limit `c` almost surely at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a` in the sense
of strict differentiability. -/
lemma integral_has_strict_deriv_at_of_tendsto_ae_left
  (hf : interval_integrable f volume a b) (hmeas : measurable_at_filter f (𝓝 a))
  (ha : tendsto f (𝓝 a ⊓ volume.ae) (𝓝 c)) : has_strict_deriv_at (λ u, ∫ x in u..b, f x) (-c) a :=

[Mario Carneiro]

Regarding filters specifically, a lot of formalizers have basically independently come to the realization that filters are amazing and make loads of things easier, and mathematics courses are lagging behind by avoiding this tool or teaching it only on the side in an advanced class. So the library reflects a version of mathematics that biases more heavily towards what others would see as a niche object.

[Sebastien Gouezel]

Also, the Isabelle/HOL example is misleading here, because the statement is probably not what you think it is: the integral it mentions is a pretty unusual one (the Henstock integral) which is well behaved for this theorem but badly behaved for most other properties. Normally, the fundamental theorem of calculus should require that f' is continuous, or at least integrable.

[Sebastien Gouezel]

And you're not talking about the same FTC (FTC-1 in one case, FTC-2 in the other case). The better analogue of the Isabelle/HOL theorem you are mentioning is docs#integral_eq_sub':

theorem integral_deriv_eq_sub' (f) (hderiv : deriv f = f')
  (hdiff : ∀ x ∈ interval a b, differentiable_at ℝ f x)
  (hcont : continuous_on f' (interval a b)) :
  ∫ y in a..b, f' y = f b - f a :=

(which is a special case of a more general theorem which doesn't require continuity). Is it that bad?

[Mario Carneiro]

I actually think the metamath formalization does rather better on both points:

ftc2.a  ⊢ (𝜑 → 𝐴 ∈ ℝ)
ftc2.b  ⊢ (𝜑 → 𝐵 ∈ ℝ)
ftc2.le ⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc2.c  ⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ))
ftc2.i  ⊢ (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
ftc2.f  ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
----
ftc2    ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

The statement is easier to recognize as the FTC from the textbooks, and the statement does not mention banach spaces or filters. The reason for this is because it's not as general of a theorem as the mathlib one, it really is just the undergrad theorem

[Kevin Buzzard]

@Apurva Nakade I think you are misunderstanding the role of mathlib.

Mathlib is not supposed to be an educational resource which we can point beginners to and say "look, here is how to do mathematics in Lean". And it is certainly not supposed to be a teaching tool where people who don't know the mathematics and/or don't know any Lean can come and learn it. In the same way, Bourbaki is a series of books, but they are not educational textbooks which are supposed to be an introduction to the subject for beginners and they are not supposed to have lucid special cases in which make comprehension easier. I think your complaints are completely understandable, but also misguided, and are furthermore off-topic and theaten to derail an interesting thread. So let me first try and say something about the issues you raise and then let me get back to the original question.

Yes mathlib might be completely unreadable and unusable for you, but I would say that if this is the case then perhaps you are not the target audience. The main point is that just because you, and most of my mathematics undergraduates, might think that the fundamental theorem of calculus is some statement about differentiating and integrating infinitely differentiable functions from the reals to the reals, the more general statement is something which a modern researcher in analysis needs to build even more complex theories on top of, so of course we prove the more general statement and deduce the classical result from it, and we are trying to make a tool which ultimately in some form will be used by modern researchers in analysis, and not a teaching tool.

So what about my poor mathematics undergraduates who don't have a clue what a Banach space is but still want to learn some analysis or want to learn some lean? Well for them we have to create different resources which sit on top of mathlib and which are written to be understandable to be completely different (and much larger) set of people. This is the point of, for example, the course I gave last year where things like limits of sequences are defined in the standard way and theorems are proved about them in the standard way, and only later in the course is the link made to filters, after a whole lot of material explaining what filters are.

If we were writing mathlib like that then I'm sure you would find it a much more beautiful object but I can be equally confident that the nature paper explaining the liquid tensor experiment would not exist and as a result the community would be in a far worse state when it comes to things like funding, because it would have far less attention from experts.

So this finally brings me back to the original question, "where are we going"? I see a future where tools running on top of Lean are used in education, from school level to PhD students. From simple proofs in geometry with some visual interface, to undergraduates working through formalised problem sheets using high-powered tactics and writing in a controlled natural language, to PhD researchers in algebraic geometry wanting to search for possibly-helpful results in a database of theorem statements, all of these things should be possible. For these things to happen, we need more tools. As Apurva has pointed out, mathlib is not that tool. However these tools, which would sit on top of mathlib rather than being equal to mathlib, are clearly within scope now and as smart people interested in mathematical education begin to understand the potential of the software, these tools will begin to appear.

[Patrick Massot]

There are a lot of different things going on here. First it's indeed true that Apurva likes the Isabelle statement because he doesn't fully understand it. Next it's true that both Isabelle's version and ours are much more advanced than the first statement of this theorem you might encounter. And indeed one can easily build teaching tools on top of mathlib. The tutorials project is an old version of my first year course using Lean. There I use a home made version of limits of sequences and functions. But it secretly uses mathlib's real numbers based on filters and when I need to use without proof Bolzano-Weirstrass in the last file I have a tiny bit of glue needed to connect to mathlib's version.

[Apurva Nakade]

Thanks for all the thoughtful answers!

[Apurva Nakade]

The tools don't only need to be educational. I'm thinking also of non-mathematicians, say a statistician, who clearly knows what vector spaces are but might find current "linear algebra" in mathlib unapproachable

[Apurva Nakade]

But I do see the points you're making. Mathlib just isn't meant for this. Thanks again.

[Arthur Paulino]

I'm on my very early days into Lean and I too have some considerations on my learning experience, not only regarding Lean itself but also about getting into computer-assisted proofs.

I agree that it makes sense for people to go through tutorials before they're able to write programmatic proofs. But for people with a lot of mathematical baggage, it might be very uninteresting to do so before they're able to understand the code. LaTeX is not a very extensible comparison because it outputs clean and beautiful portable documents, which is attractive enough. I am enjoying this learning experience because I'm into CS (a lot), but if I were a busy math researcher, with a lot to write, classes to organize, tests to formulate and correct and students to guide, I would have a strong excuse not to learn Lean or any other similar tool.

Thus, I see a big opportunity on improving the readability and attractiveness of Lean code output. More powerful hover hints, better contextualization of auto-completions etc would help a lot. Yesterday I couldn't make the direct mental link that rfl means "reflexivity", for instance. Maybe also add a "simplify" tactic (like in Coq) for the sake of clarity if the author intends to go slower? Also pretty auto-generated and interactive HTML books would be a good hook IMO.

[Johan Commelin]

@Arthur Paulino simp already exists, and is used a lot.

[Johan Commelin]

Also, I very strongly think that lack of formalized libraries is the biggest deal-breaker at the moment. All my colleagues work with things like Kähler manifolds, or triangulated categories of motives. Since those definitions are not available, they don't look further.

[Tung Tran]

A bit unrelated here, but I was a bit curious about the future of ATP in Lean. Can traditional theorem provers such as E be used in Lean the way PACT and gptf can?

[Alex J. Best]

The only major work I know of in this direction is due to @Gabriel Ebner who made a hammer for lean 3 https://gebner.org/pdfs/2020-01-08_fomm20_leanhammer.pdf . I think his conclusion was that it was a bit too slow to translate and attempt to reconstruct the proofs in lean 3, but hopefully in Lean 4 tools like this would be more usable?