Proof assistants for undergraduate analysis

Question

I am looking for a program that would help me prove some elementary inequalities. What I mean by that is that:

• I would tell the program some term written with usual functions, then I would tell him « use the Cauchy-Schwarz inequality like this », « distribute this linear function over this sum », « apply Fubini’s theorem to switch these two integrals », etc.;
• It would show me step by step what the « current term » looks like;
• When the proof is finished, it would output a text that is a program itself, such that anyone wanting to check my proof would only have to compile the program.

Now, I think that any proof assistant would allow me to do that, but is there a user-friendly one, that can be used by people that have never used any proof assistant before?

I am sure that some people working in analytic number theory (which is, as far as I know, a field where proofs are usually full of « elementary » but very, very long and subtle inequality proofs) should already be using this kind of stuff (I mean, I hope they are, this would make refereeing much easier).

EDIT: after reading Andrej Bauer’s answer, I realized that my question wasn’t precise enough.

To set an arbitrary threshold, let me give you an example: when I write proofs in $\LaTeX$ of this kind of things, I spend some time copying the current term, paste it below, make some identical changes on different terms, writing « because of Lemma 3.1 » in the margin, get worried about overfull hboxes, make some mistakes that I spot only after trying to prove three other lemmas based on this one, so I have to change everything, etc.; all this for a proof that only a few people will have the courage to check by hand. I am willing to invest a lot of time in learning how to use proof assistant that, after some effort to get proficient with it, would allow me to write automatically checkable proofs in roughly the same time as the time it takes me to typeset them into $\LaTeX$. If there is one, can you tell me which one it I would be?

I have always been afraid of learning Coq or Lean (the only ones I have heard of) because I have the (uninformed opinion) that since they have been designed for a general purpose, they might not be very nice to use for such a specific (and, to my opinion, much more elementary) purpose.

Answer 1

(I have amended the answer after the OP changed the question. I leave below the original answer for posterity.)

Your expectation that something is to be gained by having a special-purpose proof assistant is a bit misguided. It's like expecting that having a special-purpose LaTeX for analysis would bring advantages over general LaTeX. Both LaTeX and proof assistants are very flexible and can be adapted to all sorts of tasks because they are highly programmable. If there is enough interest, someone will create special-purpose tactics for dealing with inequalities (and in fact people already have, ask another question).

I would recommend that you learn Lean at this point, because it's taking over the world of formalized math quite rapidly. There are many tutorials that you can learn from. To my students I recommend the Natural numbers game, and any other one that interests them, and after that Mathematics in Lean.

Original answer: There is no proof assistant like that at present, at least not one that you will be able to use without investing some time into learning how to use it. The initial investment is similar to that of learning LaTeX, I would say.

Answer 2

As Andrej says, nothing is quite as you want, but we are getting very close, when we combine tools like formal theorem provers (like Lean), AI chat (like ChatGPT), code assistants (like CoPilot), and ITP-specific AI (like Lean CoPilot or LLMLean).

For example, say I ask ChatGPT the following:

Convert the following reasoning into Lean 4 using calc mode.

The goal is to prove $(\sum_{i=0}^\infty x_i y_i)^2 \leq \sum_{i=0}^\infty \sum_{j=0}^\infty x_i^2 y_j^2$ where $\{x_i\}$ and $\{y_i\}$ are in $\ell_2$:

$(\sum_{i=0}^\infty x_i y_i)^2 \leq (\sum_{i=0}^\infty x_i^2) (\sum_{j=0}^\infty y_j^2)$ by Cauchy Swartz

$= \sum_{j=0}^\infty \sum_{i=0}^\infty x_i^2 y_j^2 $ moving the sum inside by linearity of sums

$= \sum_{i=0}^\infty \sum_{j=0}^\infty x_i^2 y_j^2 $ swaping sums by Fubini's theorem for sums.

It responds with the following Lean code:

import Mathlib.Analysis.SpecialFunctions.Pow -- Import necessary modules

open Classical -- For classical logic, if needed

example (x y : ℕ → ℝ) (hx : summable (λ i, x i ^ 2)) (hy : summable (λ i, y i ^ 2)) :
  (∑' i, x i * y i) ^ 2 ≤ ∑' i, ∑' j, x i ^ 2 * y j ^ 2 := by
calc
  (∑' i, x i * y i) ^ 2
      ≤ (∑' i, x i ^ 2) * (∑' j, y j ^ 2) : by apply real_inner_smul_sq; exact ⟨hx, hy⟩ -- Cauchy-Schwarz inequality
  _   = ∑' j, ∑' i, x i ^ 2 * y j ^ 2 : tsum_mul_tsum_eq_tsum_double hx hy -- Move sums inside by linearity
  _   = ∑' i, ∑' j, x i ^ 2 * y j ^ 2 : tsum_fubini' (λ i j, x i ^ 2 * y j ^ 2) hx hy -- Swap sums by Fubini's theorem

Unfortunately, it is not completely correct. One problem is that ChatGPT mixes up Lean 3 and Lean 4 syntax. Also, ChatGPT doesn't have access to the Lean environment or the Mathlib documentation, so the proofs are often filled with made-up theorem names.

If I manually clean up the syntax (using a bit of basic Lean 4 experience, not too much), we get:

import Mathlib -- Import necessary modules

example (x y : ℕ → ℝ) (hx : Summable (λ i ↦ x i ^ 2)) (hy : Summable (λ i ↦ y i ^ 2)) :
  (∑' i, x i * y i) ^ 2 ≤ ∑' i, ∑' j, x i ^ 2 * y j ^ 2 := by
calc
  (∑' i, x i * y i) ^ 2
      ≤ (∑' i, x i ^ 2) * (∑' j, y j ^ 2) := by sorry -- Cauchy-Schwarz inequality
  _   = ∑' j, ∑' i, x i ^ 2 * y j ^ 2 := by sorry -- Move sums inside by linearity
  _   = ∑' i, ∑' j, x i ^ 2 * y j ^ 2 := by sorry -- Swap sums by Fubini's theorem

I omitted the proofs of each step, because again they didn't seem correct. And even with my simple searching I couldn't find the needed lemmas. (I didn't try more advanced AI like Lean Copilot or LLMLean.)

But you can already get a feeling for how existing theorem provers like Lean, along with a combination of AI tools could really start to fit the vision you laid out.

Until that time, I think learning Lean/Mathlib (or Isabelle/AFP, or Coq/MathComp) would start to bring you a lot of the way there. And existing AI tools like ChatGPT or Copilot already help with this translation!

---

Also, as you point out, many of the techniques in analysis are well-established, common, and elementary, so even if Lean’s Mathlib currently doesn’t have the needed lemmas or if AI tools can’t easily find them, that will soon change as more and more of these arguments are formalized in Lean (manually or automatically). Indeed, I think analysis is an area very ripe for building up AI auto-formalization specifically because of these properties of analysis proofs.