19
votes
Accepted
What work has been done on computationally intensive proofs?
You are touching upon some questions that we are currently investigating in our research group, but we do not have definite answers yet, so let me just make a couple of comments regarding the trade-...
- 11k
18
votes
Accepted
Tools for checking the consistency of a type theory
One can think of type theory as an algebraic theory on steroids (there is technical merit to this claim). Every algebraic theory has a model, namely the trivial one whose carrier is the singleton. A ...
- 11k
15
votes
Accepted
Are there any well-known Internal DSL Proof Assistants?
As Alex Nelson pointed out, I think this is exactly the LCF approach to theorem proving. See The LCF Approach
to Theorem Proving for details.
HOL-Light would certainly fit this description. You ...
- 10.3k
15
votes
Proof Assistants with support for creating executable software artifacts
You speak of program extraction, but if your main goal is to prove correctness of effectful programs, you might consider programming languages that allow you to write code directly, and prove it ...
- 11k
14
votes
Are there any well-known Internal DSL Proof Assistants?
If you are asking about a kind of embedding advanced proving facilities into modern System F$_\omega$-wannabe languages then I would suggest you to take a look onto Proving Ground base library for ...
- 1,307
14
votes
What games are there?
Cubical Agda suggestions
The HoTT game
The HoTT Game was written by some Imperial undergraduates; the goal is to prove that the fundamental group of the circle is the integers, in cubical Agda. You ...
14
votes
What games are there?
Lean suggestions
The max minigame
Short online game here. Something I knocked off with a couple of collaborators when we were trying to work out how to make a real number game. We still haven't got to ...
11
votes
Accepted
Is there a Mizar-like sublanguage for Coq?
There indeed used to be a "declarative language for Coq" often referred to as Czar, but it was removed (from Coq's core) a long time ago. If it had had any actual users, it would have been ...
- 657
11
votes
What games are there?
The incredible proof machine proof-machine is a game with a collection of theorems for classical propositional logic, classical first-order logic, and the simply typed lambda calculus.
Example (think ...
11
votes
Accepted
Proof assistants or libraries in proof assistants for working with model theory
First, recall that model theory (of FOL) is just mathematics about certain types of mathematical objects, "structures" as they are defined in model theory. So it isn't really any more ...
- 10.3k
11
votes
Proof Assistants with support for creating executable software artifacts
Lean 4 is both a proof assistant and general-purpose programming language, with built-in native code generation.
...
- 1,722
11
votes
Are there any well-known Internal DSL Proof Assistants?
I can't speak to how well-known it is, but holpy[1] is a fairly recent library that implements higher order logic in Python. The main selling points they describe in the arXiv paper are a "point ...
- 215
10
votes
Accepted
Are there any proof assistants or theorem provers based on the method of analytic tableaux?
I take it you already know the answer to this.
HOL Light was written by John Harrison (ref) who also authored "Handbook of Practical Logic and Automated Reasoning". (site) Think of the book ...
- 2,856
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,607
10
votes
Proof assistants or libraries in proof assistants for working with model theory
Lean powers https://flypitch.github.io/ which formally verifies the independence of the continuum hypothesis.
Some of that material is currently being ported to mathlib's ...
- 786
9
votes
Accepted
Toy proof assistants with very small codebases
Here are some that I am aware of:
A Tutorial Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra, implemented in Haskell, has an accompanying ...
- 11k
8
votes
What work has been done on computationally intensive proofs?
Not as general as Andrej's answer but more a data-point for your interest. We've been looking at how to construct formal proofs about neural network-enhanced systems in proof assistants. This runs ...
- 191
7
votes
Accepted
Are there any provers based on a paraconsistent logic?
I am not sure this is the answer you are looking for, but here it is anyways.
In the proof-as-program paradigm embraced by dependent type theory, inconsistency is not necessarily an issue. Indeed, one ...
- 2,393
7
votes
Accepted
verifying combinatorial constructions - choice of a proof assistant
If I understand you correctly, you will be working with finite discrete objects, such as finite fields, finite groups, finite combinatorial objects, etc. I would recommend using a proof assistant ...
- 11k
7
votes
Accepted
Libraries of formally stated theorems with proofs verified by humans
If I understand correctly, I think you want libraries of formal theorem statements without proofs. Check out the proposed formal abstract project from Tom Hales. That is his goal, but it hasn’t got ...
- 10.3k
7
votes
Are there any non-English based proof assistants?
The System for Automated Deduction can check proof texts both in English and Russian if I remember correctly: SAD
Translating keywords is of course an easy task, but it'd be interesting to see if ...
- 665
5
votes
Are there any well-known Internal DSL Proof Assistants?
This is indeed the LCF approach, and is how the various HOL systems operate to this day. Typically, the systems do augment or fiddle with their underlying programming language implementations. For ...
- 1,142
5
votes
Accepted
Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?
Your XY problem
Let me step back and think about the XY of your problem. You have a category theory solver which already generates "proofs" and you want to export those proofs to be checked ...
- 10.3k
4
votes
Proof Assistants with support for creating executable software artifacts
HOL4 + CakeML support generation of verified machine code guaranteed to be equivalent to the semantics of the input program. There are techniques for
verifying the input program at the level of ...
- 1,142
4
votes
Are there any proof assistants or theorem provers based on the method of analytic tableaux?
(Turning my comment to an answer, but downvote if I've misunderstood.)
Is this the same as connection tableau? If so there are a number of light-weight automated theorem provers for FOL which use ...
- 10.3k
4
votes
Are there any non-English based proof assistants?
I point you to MMP/Geometer, by Xiao-Shan Gao.
This system allows you to prove geometric theorems, even through a graphical interface.
The commands on the shell are in English, the GUI is mainly in ...
- 363
4
votes
verifying combinatorial constructions - choice of a proof assistant
I moved this answer to Proof assistants for beginners - a comparison, since it is general advice. However, I still do think it applies to your circumstance. In particular, it is not clear in your ...
- 10.3k
4
votes
Accepted
Generating valid statements without a proof goal
This definitely falls under various active research projects to find interesting mathematics from a set of theorems. I can't point to a particular project per say, but let me mention why this is so ...
- 10.3k
4
votes
Which proof assistants implement Church's rule?
Not the answer you would like to hear, but that would be "no proof assistant" (to my knowledge). The first reason is that Church's rule does not hold for classical theories but the ...
- 11k
4
votes
Accepted
Checking if a goal is *definitely wrong* by testing it against random examples in Coq
QuickChick recently got a tactic that you can call in the middle of a proof.
...
- 2,242
Only top scored, non community-wiki answers of a minimum length are eligible