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.
27
questions
4
votes
1
answer
93
views
What is the best way to learn Iris completely independently
I am looking forward to learning Iris by myself, I have essential basic knowledge of Coq and logic but I don't know where to start. Logically, I looked into materials on the project website; the video ...
5
votes
1
answer
452
views
Examples of theories where tactic language is required for simple proofs
I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
- 158
0
votes
1
answer
54
views
Is the Archive of Formal indexed in journal databases?
I was wonder if journals that publish regularly formal proofs are indexed in journal databases like Scopus or Web of Science. Apparently, this is not the case. Why is it so?
- 101
6
votes
1
answer
244
views
(Dis)Advantages of basing a proof assistant on CH correspondence?
Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
- 273
2
votes
0
answers
84
views
Algebraic manipulation: what is the best tool?
I have a set of algebraic axioms. I need to prove an equation, an algebraic law. What I did was applying "trivial" rewrite rules by a theorem prover from both ends, and then an automatic ...
- 267
2
votes
0
answers
74
views
Formally verified email or communication?
This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway.
I would like to consider the simplest possible formally verified ...
- 175
4
votes
1
answer
103
views
How do we know that we can trust proof assistance to produce correct results?
Well, pretty simple question, how do we know that we can trust the proof assistants? I ask this question as a complete lay in proof assistants. Maybe a trivial answer could be "because smart ...
7
votes
2
answers
1k
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 ...
- 357
3
votes
2
answers
355
views
Are there minimal typed proof verifiers that can deal with the majority of mathematics?
I would like to know if there are proof verifiers that can deal with the majority of mathematics (definitions, theorems, proofs with verification), while also having a minimal implementation. I am not ...
- 131
1
vote
0
answers
42
views
How do I prove this property about a factorial specification in Coq?
Notes: This post got pretty long... my apologies but hopefully somebody can take the time to look through it. Also, some of the code below uses terms that are defined elsewhere in my file and not ...
1
vote
1
answer
64
views
How do I prove an expression in Coq that involves pattern matching?
I'm working on a proof in Coq and my proof state is as follows:
...
3
votes
0
answers
42
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 ...
- 131
1
vote
2
answers
915
views
Make ChatGPT write formal proof from natural language proof
I know very little about proof assistants, but I played a little with Lean, so I have some basic knowledge of how they work.
I was curious whether I could make ChatGPT convert some natural language ...
- 121
6
votes
1
answer
410
views
Paths Between Quotient Types in Cubical Agda
I'm new to Cubical Agda and I am trying to define the dependent set eliminator for certain quotient types.
In particular, my quotient type is the integers, quotiented by the absolute value function (<...
- 61
5
votes
1
answer
108
views
Is there any formalization (with any theorem prover) of the Bohm theorem for lambda-calculus?
I am an university student working on a thesis about λ-calculus. I'd like to know if there's any article or publication about proof assistant formalizations of the Bohm theorem ("any two normal ...
4
votes
3
answers
205
views
are there any standard proof formats?
I would like to know if there are any proof formats which is used to exchange proofs among proof assistants. I realize different proof assistants use different foundations but for those that have the ...
- 43
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.
...
- 348
3
votes
1
answer
109
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 ...
- 269
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
132
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 ...
- 269
9
votes
2
answers
673
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 ...
- 93
3
votes
1
answer
124
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?
- 176
5
votes
1
answer
78
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
335
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 ...
- 111
6
votes
1
answer
183
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
20
votes
0
answers
217
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,447
25
votes
2
answers
345
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 ...
- 722