Skip to main content

Questions tagged [automated-theorem-proving]

For questions regarding ATP's (Automatic Theorem Provers), which attempt to prove a theorem without any assistance. If you are using a Proof Assistant or an interactive theorem prover and are providing help to the prover, then do not use this tag.

Filter by
Sorted by
Tagged with
-3 votes
0 answers
57 views

What are some examples of very large term enumerations of a proof assistant language?

I’m just curious to know of significant instances of brute force, total enumeration of all terms in a logical theory. For example, enumerating every term of ZFC - how far has anyone gotten? What are ...
Julius Hamilton's user avatar
1 vote
0 answers
44 views

Integrating SAT solvers supporting only a finite set of variables into proof assistants

We're currently looking at how to integrate neural network solvers into general proof assistants. One of the issues we're running into is that, unlike general SAT/SMT solvers like Z3, queries for ...
Matthew Daggitt's user avatar
4 votes
2 answers
168 views

Ltac - run tactic for each hypothesis of given pattern

Especially in the context of lia, which can sometimes fail to prove a theorem in the form of forall x, x <> 0 -> P x ...
shooqie's user avatar
  • 171
4 votes
1 answer
103 views

Using proof assistants to analyze probabilistic models (identifiability in particular)

I recently had an idea that proof assistants/theorem provers might be useful for static analysis of probabilistic models. My familiarity with proof assistants/theorem provers is shallow (some intro in ...
Martin Modrák's user avatar
4 votes
3 answers
257 views

How does Z3 "exhaustively search" real numbers?

I was looking at this tutorial: https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb#scrollTo=4yuA2Fry68Y6&line=4&uniqifier=1 . It says "Proof = ...
llllvvuu's user avatar
  • 143
3 votes
0 answers
44 views

How do proof assistants/ automated theorem provers compare with other symbollic tools like mathematica, maple or magma in terms of practicality [duplicate]

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 ...
userrandrand's user avatar
2 votes
1 answer
283 views

Eliminating "Exists Unique" in Lean 3

In Lean 3, similar to this question, I want to exhibit a witness of $x$ of $P(x)$, given that $\exists x,P(x)$. The difference is that I can also prove $\exists! x,P(x)$, so there is exactly 1 element ...
Zongshu Wu's user avatar
3 votes
1 answer
119 views

Do implementations of a PA and of ATP have overlap?

I'm wondering how much overlap (read: code-reusage) there is between a PA and an ATP system. Are they based upon the same type system at least? I'm wondering, because right now I'm working on ...
Daniel Donnelly's user avatar
-3 votes
1 answer
149 views

Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?

So I'm not sure how things are done in Lean4 or Coq, but I'm interested in their search features. For example, "Search for all theorems that get satisfied given a user-defined list of ...
Daniel Donnelly's user avatar
11 votes
1 answer
455 views

auto-generating the proof of infinitude of primes

The chess computer which beat the human world champion in 1997 had a huge database of openings inbuilt into it. However my understanding of Deep Mind's alpha zero is that it is capable of generating ...
Kevin Buzzard's user avatar
7 votes
0 answers
78 views

Is any theorem prover able to prove quadratization relations without knowing the proof strategy that humans used?

Motivation In discrete optimization, our goal is often to optimize a function of binary variables, such as: $$\tag{1} {\scriptsize 5 - 3b_1 - b_2 - b_3 + 2b_1b_3 - 3b_2b_3 + 2b_1b_2b_3 - 3b_4 + ...
Nike Dattani's user avatar
  • 1,165
12 votes
0 answers
197 views

Do any automated theorem provers have the ability to stop, save state, reboot computer, restore state, continue?

With automated theorem provers knowing ahead of time how long the search will take or even if it will find a solution is unknown. Often for long running searches one eventually just has to halt the ...
Guy Coder's user avatar
  • 2,836
8 votes
1 answer
388 views

What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?

This paper describes a theorem generator called MetaGen. MetaGen's purpose is to make larger training sets to train provers, by producing theorems similar to ones a human might select for inclusion in ...
Greg Nisbet's user avatar
  • 2,741
7 votes
1 answer
136 views

Understanding "saturating" theorem provers

The documentation for the E Theorem Prover explains this as the first step in its process: A clausification algorithm translates first-order input into clause normal form, such that the resulting ...
Reubend's user avatar
  • 519
9 votes
2 answers
268 views

Are search heuristics the main bottleneck for automated theorem provers?

My understanding of most automated theorem provers (which is possibly an incorrect understanding!) is that they start with some premises stored as unprocessed statements, and repeatedly select one to &...
Reubend's user avatar
  • 519
15 votes
1 answer
263 views

Are there automated theorem provers for constructive logics? What strategy do they use?

I know of a handful of automated theorem provers for classical first-order logic such as Vampire (source code). Internally, I think most of these provers work by translating premises and the negated ...
Greg Nisbet's user avatar
  • 2,741
24 votes
2 answers
595 views

Successes of machine learning in formal theorem proving

Attempts to apply machine-learning (as opposed to hand-crafted automation) to formal theorem proving are still in their infancy. Still, there have been some successes. GPT-f found some proofs that ...
Will Sawin's user avatar