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.
5 questions
10
votes
2
answers
801
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 ...
- 259
2
votes
1
answer
205
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 ...
23
votes
1
answer
358
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,709
8
votes
2
answers
2k
views
Is it possible to make a proof assistant program based on ZFC?
I heard that many proof assistant programs are made based on the type theory.
For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it.
So I have a question.
Is it ...
- 407
6
votes
3
answers
2k
views
Proof assistants for undergraduate analysis
I am looking for a program that would help me prove some elementary inequalities. What I mean by that is that:
I would tell the program some term written with usual functions, then I would tell him « ...
- 163