Skip to main content

Questions tagged [software-request]

This tag is used for questions that ask for software with a certain property or goal, such as automated theorem provers for equational logic. If the question is not specifically for software consider using the tag by reference-request.

Filter by
Sorted by
Tagged with
32 votes
2 answers
2k views

What work has been done on computationally intensive proofs?

Fifty years ago, few would have imagined that the process of verifying the correctness of a known proof of a mathematical theorem might be so costly that the mathematical community would hesitate to ...
Timothy Chow's user avatar
16 votes
2 answers
197 views

Are there any proof assistants or theorem provers based on the method of analytic tableaux?

Are there any proof assistants or theorem provers based on the method of analytic tableaux? A closed tableau makes the branching structure of a proof using case analysis very obvious. I like tableau ...
Greg Nisbet's user avatar
  • 2,869
15 votes
4 answers
396 views

Are there any well-known Internal DSL Proof Assistants?

Proof assistants like Coq have their own extensible syntax that's rather different from a general purpose language. I'm curious whether there are any well-known proof assistants that are implemented ...
Greg Nisbet's user avatar
  • 2,869
15 votes
4 answers
472 views

What games are there?

A game is a fun interactive tutorial/puzzle/challenge that provides the user with a DAG of definitions, theorem statements, examples, etc. and asks the user to prove all the theorems in this DAG. For ...
15 votes
1 answer
266 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,869
14 votes
4 answers
275 views

Proof Assistants with support for creating executable software artifacts

I am looking for proof assistants with which I can write sound proofs about my functions and values, as well as compile actions of type IO () into executable code. ...
Agnishom Chattopadhyay's user avatar
14 votes
2 answers
320 views

Tools for checking the consistency of a type theory

My question is twofold: How do you define consistency (analogously to the concept in first-order logic) in the context of a type theory? Are there any tools that can check consistency? I have seen a ...
Greg Nisbet's user avatar
  • 2,869
13 votes
2 answers
202 views

verifying combinatorial constructions - choice of a proof assistant

The choice of the proof assistant to use for formalisation depends on the area quite a bit; e.g. they say that algebraic topology comes easy in HoTT assistants. What would be the most natural choices ...
Dima Pasechnik's user avatar
11 votes
2 answers
120 views

Proof assistants or libraries in proof assistants for working with model theory

The basics of model theory contain, as far as I understand, some theorems that are difficult to prove in their full generality. For example, the compactness theorem in FOL for languages with ...
Greg Nisbet's user avatar
  • 2,869
10 votes
1 answer
264 views

Is there a Mizar-like sublanguage for Coq?

Isabelle has the frontend Isar which mimics some features of the Mizar system. I'm curious if Coq has anything similar, i.e. an alternative to tactic scripts that's designed to be readable or similar ...
Greg Nisbet's user avatar
  • 2,869
10 votes
2 answers
239 views

Are there any non-English based proof assistants?

There is a Wikipedia article about non-English based programming languages, but what about for proof assistants? I recall seeing one which was a translation of Lean tactics to French, by Patrick ...
Jia Ming جيا ميڠ's user avatar
10 votes
0 answers
187 views

Is there a proof assistant (or an embedding) for the (co)end calculus?

A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
Trebor's user avatar
  • 4,015
9 votes
1 answer
178 views

Generating valid statements without a proof goal

Given some initial list of assumptions, I'd like to generate some true statements which follow from them without seeking a specific proof goal. I only need a small number of consequences from those ...
Reubend's user avatar
  • 519
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
5 votes
2 answers
179 views

Are there any provers based on a paraconsistent logic?

This question talks about controlled usage of a self-containing top type satisfying $\text{type}\! : \text{type}$. I'm wondering if there are any provers that deliberately give $\text{type}\!: \text{...
Greg Nisbet's user avatar
  • 2,869
5 votes
1 answer
138 views

Libraries of formally stated theorems with proofs verified by humans

This answer by Kevin Buzzard talks, among other things, about incremental progress made in Lean's mathlib vs Isabelle. There's a lot in that answer that I don't understand, but one thing that seems ...
Greg Nisbet's user avatar
  • 2,869
5 votes
1 answer
183 views

List of general purpose Coq sublanguages for defining custom tactics

I've been tweaking the Coq plugin template recently to try to get a feel for writing custom Coq tactics in OCaml. It's tricky. You need to define an .mlg file (...
Greg Nisbet's user avatar
  • 2,869
5 votes
1 answer
178 views

Is there an easy-to-learn GUI of proof assistants for teenagers in maths education?

I'm a high school sophomore and I have been interested in Interactive Theorem Proving for a year or two. I found it extremely hard for my peers (lack of knowledge in mathematical logic, type theories ...
Chesium's user avatar
  • 51
4 votes
2 answers
185 views

Which proof assistants implement Church's rule?

Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive ...
Christopher King's user avatar
2 votes
1 answer
150 views

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?

I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
HighAsAKiteOnMath's user avatar
2 votes
1 answer
54 views

Checking if a goal is *definitely wrong* by testing it against random examples in Coq

I'm currently poking around in a medium-sized Coq codebase that I didn't write and am not very familiar with ... and I'm trying off and on to make progress on some lemmas where the proof attempt was <...
Greg Nisbet's user avatar
  • 2,869
2 votes
0 answers
65 views

Have Hyperdoctrines been formalized?

I was thinking of formalizing them myself for a project if they haven't been already, and I looked in libraries and couldn't find anything. I was thinking of coq in particular because it's the only ...
Julián's user avatar
  • 143
2 votes
0 answers
68 views

Tool for typing mathematical physics, e.g. differential geometry

Many expressions in mathematical physics use a rather sloppy notation, e.g. the Lie bracket on a vector field is defined using ambiguous notation, where $X : M \rightarrow TM$ is first defined as a ...
user2361's user avatar
1 vote
0 answers
61 views

Embedding proof assistance in an application

Context Perhaps this is too open-ended a question for StackExchange, in which case I apologize, but otherwise here goes: I have a project I'm toying around with, the core of which is what I'd call &...
Eric Anderson's user avatar
-1 votes
1 answer
104 views

Implementability of proof assistants for Infinitary logics with finite many terms

Infinitary logic is a natural consequence of extending the length of proofs of first-order logic to a infinite ordinal level. By definition, since proof lengths are infinitely long, one should not ...
Ember Edison's user avatar