14
votes
Successes of machine learning in formal theorem proving
Only a bit more than two months ago, a new formula for Kazhdan-Lusztig
polynomials was found by Google's deep learning subsidiary: DeepMind (the same machine-learning company that wrote AlphaGo to ...
- 1,175
11
votes
Accepted
auto-generating the proof of infinitude of primes
I doubt you are out of date. I think given a reasonable interpretation of this question, this is well beyond current (2022) systems.
Nonetheless, I will also argue your question needs some ...
- 9,653
10
votes
Accepted
Are there automated theorem provers for constructive logics? What strategy do they use?
The firstorder tactic in Coq is an "experimental extension of tauto to first-order reasoning." The tauto tactic &...
- 1,547
8
votes
Successes of machine learning in formal theorem proving
The group at OpenAI has recently published a new paper, among other problems they have been able to prove two questions from the International Mathematical Olympiad. Isabelle's Sledgehammer has been ...
- 665
7
votes
Accepted
What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?
MetaGen may be unique in that it is a Neural Theorem Generator which generates both statements and proofs.
Nonetheless, there are a number of other papers which do 2 of the 3: Neural, Generate ...
- 9,653
6
votes
Accepted
Understanding "saturating" theorem provers
The basic idea is we want to check if a formula $\varphi$ is satisfiable. This is analogous to checking there exists a row in the truth-table for a proposition for which the proposition is true. First-...
- 1,574
6
votes
Accepted
Do implementations of a PA and of ATP have overlap?
Unfortunately there is much less code reuse possible than one would hope.
There three levels to consider:
Differences between mathematical foundations (and implementations) between proof assistants.
...
5
votes
Accepted
Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?
Building that gigantic proof graph as an explicit graph would probably be a very bad idea, given its size and the complexity of "connecting inputs to outputs". Indeed, as you can have an ...
- 5,620
5
votes
Are search heuristics the main bottleneck for automated theorem provers?
Automated theorem provers rely on the resolution algorithm because it is complete. This means that if a proof exists, the prover is guaranteed to find it. Resolution works as follows:
Say you want to ...
- 2,320
5
votes
Are search heuristics the main bottleneck for automated theorem provers?
I used to feel the same way.
My dream was a computer that would give me the answers I wasn't able to reach because I wasn't smart enough.
Now I no longer hope that such a thing is possible; in fact, ...
- 363
3
votes
How does Z3 "exhaustively search" real numbers?
It does not "exhaustively search" real numbers by checking them one by one (obviously). Instead it uses sophisticated algorithms that use lots of algebra to do it.
Let me give a simple ...
- 9,931
3
votes
Accepted
How does Z3 "exhaustively search" real numbers?
SMT is exhaustively searching in the S (SAT), not necessarily in the MT (theory).
Let's dig a little deeper into what an SMT solver actually is: SAT-modulo-theories. That means, it can solve boolean ...
- 991
3
votes
Ltac - run tactic for each hypothesis of given pattern
Another way to do this is to check for the hypothesis that you're inserting. I use this pattern pretty commonly.
...
- 304
3
votes
Ltac - run tactic for each hypothesis of given pattern
Perhaps the base case is just missing in your implementations as recursive tactics.
...
- 673
1
vote
Using proof assistants to analyze probabilistic models (identifiability in particular)
I would say this is definitely reachable, but nowhere easy.
As your last question suggests, you would like to use proof assistants compared to other tools because they give you more assurance. This is ...
- 5,620
1
vote
How does Z3 "exhaustively search" real numbers?
This is the area of decision-procedures; a field with tons of research and a huge literature. To put it shortly, z3 (or any other SMT solver) does not exhaustively go over all possible inputs, neither ...
- 119
1
vote
Accepted
Eliminating "Exists Unique" in Lean 3
First, in general you do need the axiom of choice (or a derivative theorem). Unique choice doesn't follow from the base rules of Lean, unlike ZF and univalent foundations. Also, Lean is very minimal ...
- 9,653
Only top scored, non community-wiki answers of a minimum length are eligible