# 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.

33 questions
Filter by
Sorted by
Tagged with
1 vote
129 views

I'm an undergraduate student in my final year studying applied mathematics. To graduate, I need to present a thesis, and I'm considering using Lean and first-order predicate logic for my thesis. My ...
• 111
1 vote
62 views

### How to choose an axiom system in Isabelle/HOL?

First of all, sorry if my question is too nonsensical and naive, I'm just getting started with Isabelle/HOL. I am reading Hou's "Fundamentals of Logic and Computation: With Practical Automated ...
• 111
1 vote
56 views

### Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix)

It might be a very silly question for the logic gurus but less so for me. First I generally describe the issue, than I provide a proper example with code. Assume three streams of nats: xs, ys, zs. ...
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 ...
120 views

### Proving "proof methods" as theorems in type-theory based proof systems

For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as add_assoc : forall (x y : T), x + y + z = x + (y + z). We can thus prove ...
67 views

### Research methodology in formal verification

Is there a written account on how to carry out research in formal verification with proof assistants? Formalisation of standard mathematics, verification of information systems and developing proof ...
• 311
169 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 ...
551 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 ...
• 177
1 vote
127 views

### Is the Archive of Formal Proofs indexed in journal databases?

I was wondering 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?
• 111
327 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 ...
• 313
104 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 ...
• 311
81 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 ...
113 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 ...
• 269
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 ...
• 377
453 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
48 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
148 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: ...
45 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
1k 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 ...
• 131
493 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
120 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 ...
222 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 ...
• 53
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. ...
• 358
122 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 ...
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 ...
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 ...
916 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 ...
135 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
81 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
441 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 ...
• 229
197 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
233 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,537