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
