Questions tagged [proof-assistant]

A proof assistant, or interactive theorem prover, is a software tool to assist with the development of formal proofs by human-machine collaboration.

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

Why are these two proofs so different?

I was messing around with toy lemmas in Idris and came up with this silly proof. ...
  • 73
4 votes
1 answer
81 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 ...
10 votes
2 answers
2k views

How can we formalize a game where each player is a program having access to opponent's code?

How can we define in a proof assistant (eg., Coq) a notion of a 2-player game, where each player is a program that has access to the opponent's source code? Background: In Open Source Game Theory, we ...
1 vote
1 answer
94 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 ...
9 votes
2 answers
319 views

Learning Math Proof via Proof Assistants

I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my ...
3 votes
1 answer
110 views

Difference between implementation and formalisation in a proof assistant

Some authors refer to their works as "implementation of the theory in (let's say) Agda", some refer as "formalization of the theory in Agda". What is the difference between them?
5 votes
1 answer
64 views

Semantics verification of an LTL fragment logic

I am a beginner to Isabelle and I went over the proof documentation. I am trying to implement a fragment logic of LTL over finite intervals and finite traces called MLTL, the syntax and semantics can ...
  • 53
9 votes
2 answers
220 views

Comparison between proof assistants for coinductive structures and proofs

I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction? My motivation is that I'd like to formalize some proofs, basically about ...
6 votes
1 answer
166 views

Tools to formally verify programs written in languages supported by the GNU Compiler (GCC)

Is there a website that maintains a list, or is there a list, of tools that support verification of programs written in languages supported by the GCC compiler front ends: C, C++, Objective-C, Fortran,...
  • 242
19 votes
0 answers
193 views

What is known about performance bottlenecks in proof assistants?

Background In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for ...
  • 1,237
22 votes
2 answers
262 views

How to use a proof assistant to reason in a topos?

I would like to use a proof assistant to reason in the internal language of a topos. More specifically, I would like to (be able to) formalise informal arguments such as in Ingo Blechschmidt's PhD ...
  • 518