3
$\begingroup$

TLDR

What are the advantages and disadvantages of using a proof assistant when compared to using tools like Mathematica in terms of practicality and usability/ease of use ?


ChatGPT summary of the text below

(I slightly modified it)

The author is considering learning Lean to explore AI-assisted proofs and whether it would be useful for their research. They are unsure about the practicality of proof assistants compared to tools like Mathematica, Maple, and Magma. They have doubts about the sufficiency of the knowledge base, the efficiency of proof assistants in intense computations, and what kinds of problems are better suited for proof assistants. They are also unsure if the typical problem they encounter would be solved faster by interactively using other tools. However, they see advantages in theorem searching, high-level abstractions of complex mathematical statements, and obtaining counterexamples using proof assistants.

Key Points

  • The knowledgebase in a given proof assistant may not be above or similar to that of tools like Mathematica, Maple, Magma.

  • It is unclear whether proof assistants can be used for intensive computation.

  • It is presently unclear what kinds of problems are better suited to proof assistants rather than working through the problem using Mathematica, etc.

  • Even if there exists a means to automatically solve a problem using a proof assistant, the typical problem may not be solved faster interactively using Mathematica, Maple, or Magma.

  • Advantages of proof assistants include theorem searching, high-level abstractions of complex mathematical statements, and obtaining counterexamples.


Context

I learned about Lean from meta's research on combining it with AI as shown here: https://arxiv.org/abs/2205.11491. I am hesitating to try to learn Lean to play with AI-assisted proofs and to explore whether I would find it useful for the kind of problems I am interested in.

Skimming through the article (A formally verified proof of the prime number theorem)[https://arxiv.org/abs/cs/0509025#] some of the parts look like they could have been done in Mathematica but perhaps the parts involved in defining theorems and connecting them would be difficult with Mathematica.

Overall, I understand that theorem provers are a useful means for verifying statements but it is unclear how I should use them in the process of research.

Doubts

Is the Knowledgebase sufficient to be practical on average ?

It is unclear to me whether the knowledgebase in a given proof assistant is above or similar to that of tools like Mathematica, Maple, Magma.

For example, Magma's knowledge of groups, Maple's knowledge of differential equations, and Mathematica's large database of functions. This is a difficult question to address as it depends on the area of interest. The information seems to be here: Where can I find lists of theorems that have been verified?. But I would have to do a long research to come to a conclusion. Perhaps, this can not be answered here as it might be opinion based. However, for example, this article Building the Mathematical Library of the Future states that at least in 2020, lean did not have a library for complex analysis. It is hard to convince myself to learn a language for mathematics that does not have all of undergraduate-level math.

How efficient these systems are in intense computations?

It is unclear to me whether proof assistants can be used for intensive computation. It seems no judging from the answers here: https://proofassistants.stackexchange.com/a/1162/2252.

What kinds of problems are better suited for proof assistants as opposed to software for symbolic manipulations?

Although I understand that proof assistant provide a formal means to prove something without having to resort to natural language, for the purpose of simply completing a task independently of whether it is written formally or not, It is presently unclear to me what kinds of problems are better suited to proof assistants rather than working through the problem using Mathematica, etc.

Speed of setting up the problem

Even if there exists a means to automatically solve a problem using a proof assistant, I am not sure if the typical problem I would encounter would be solved faster interactively using Mathematica, Maple, or Magma

Some advantages I could see for proof assistants

Theorem searching

I believe there is a component where proof assistants search for relevant parts of mathematics which that alone could be very useful in combination with semantic search (encoding text into a vector using a neural network where nearby vectors are semantically related). I suppose the rest is mainly a brute force tree search of combining lemmas but I do not know.

High-level abstractions of complex mathematical statements

I do not know if this is possible, but it seems that one can add lemmas and theorems in proof assistants and that those can be used to deduce statements. Perhaps one can also define theories and concepts that would allow thinking about a problem at a higher level of abstraction perhaps similar to an object-oriented language. For example, using the Cayley-Hamilton theorem as a component in deducing some further statement.

Obtaining Counterexamples

From some of the examples from lean on GitHub, if I remember correctly, it seems one can produce counterexamples to claims using proof assistants. This seems quite useful. For algebraic relationships, there is FindInstance in Mathematica that can find examples of numbers that very a constraint but that seems like just a subset of all possible counterexamples in all domains of mathematics

$\endgroup$
12
  • $\begingroup$ Tools that have different purposes cannot be compared at all for practicality. $\endgroup$
    – Trebor
    Apr 1, 2023 at 3:04
  • $\begingroup$ @JasonRute thank you indeed i think it is a duplicate. I think I searched for Mathematica and maybe Maple but I should have also searched for cas or computer algebra $\endgroup$ Apr 1, 2023 at 15:41
  • $\begingroup$ @JasonRute should i delete the post or should I leave it to redirect to that link for other people that might search for mathematica or maple ? $\endgroup$ Apr 1, 2023 at 15:42
  • $\begingroup$ If you agree that answers your question, leave it up and we will flag it as duplicate. $\endgroup$
    – Jason Rute
    Apr 1, 2023 at 15:45
  • $\begingroup$ @JasonRute the answers do define and separate CAS and proof assistants, but the message I got from those answers were that proof assistants are not particularly useful for discovering/tinkering with math as it is mainly a tool for formally setting up proofs. While that may be the main aspect, I am not sure this is true given my first example of using AI for discovering math. I still think proof assistants could be used for exploration particularly searching through a large database as mentioned in my post. $\endgroup$ Apr 1, 2023 at 15:59

0