Mathematics Stack Exchange
Mathematics Stack Exchange

Questions tagged [automated-theorem-proving]

For questions regarding the different ways to generate and verify theorems via specialized computer languages, algorithms, and other computer-aided tools.

For questions regarding the different ways to generate and verify theorems via specialized computer languages, algorithms, and other computer-aided tools.

Topics (between others): auto-generated theorems, automatic tools, computer verification, algorithms to verify theorems, declarative proof languages, etc.

118 questions
9
votes
4 answers

Why isn't math completely solved by expert systems?

Everything in math can be perfectly defined or formalized. And we could derive logical conclusions from that. However, mathematicians still use human natural language to solve their theorems. Why isn't automatic proof checking or automated theorem…
Hector Babeco
  • 91
6
votes
2 answers

Algorithm to find a proof of every provable theorem.

I found this pdf while searching on automated theorem provers: https://www.math.ucdavis.edu/~greg/145/notproof.pdf It says: "Proof by rote algorithm Non-proof courses in mathematics generally teach algorithms to do calculations. It would be nice if…
user162208
  • 61
2
votes
0 answers

Is it useful to learn to use automatic theorem provers?

I mean, do ATP's spot some obvious errors in computations or proofs? And if I'm not sure about the correctness of some modern proof found in some article, say for example Mochizuki's proof of the ABC conjecture, can I verify the correctness of the…
beginnermathematician
  • 21
2
votes
0 answers

Can we prove every provable statement with lean?

I just discovered Lean and using computers for stating and proving theorems. The first question that came to my mind, can we write any proof with Lean? Or are there limitations (something that you can write a proof for on paper but not in Lean)? I'm…
Hatchi Roku
  • 187
  • 7
2
votes
1 answer

Equivalent statements

If one looks at the directed graph of all theorems proved, let there be a vertex between statement A and B directional if A implies B, ideally it will connect results across different fields. Is there any existing system, by computer or not,…
user61606
  • 27
1
vote
0 answers

Cone relations and equivalence relations in the Myhill - Nerode Theorem.

Fix an alphabet ${\bf S}$ and a language $L \subset S^*$. For any two words $w$, $w'$ $\in S^*$, define a relation $w \sim w'$ if and only if Cone$(w)$ = Cone$(w')$. Then prove that this is an equivalence relation on $s^*$ and rephrase the Myhill -…
Barb
  • 11
0
votes
1 answer

Who to define the meta-function using induction prinicple?

I'm a beginner in Automated Theorem Proving, and I want to proof using the induction principle from the syntactic definition of propositional formulae, define the meta-function $V[\phi]$ which gives set of propositional variables of the…
Laurentiu
  • 3