# Tag Info

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

If I may offer a bit of general advice to all who are asking “where do I find a proof assistant whose foundation precisely matches the one I need“: you do not need an exact match, just one that is ...
• 9,553
Accepted

### Is it possible to make a proof assistant program based on ZFC?

There are three major foundations to theorem provers. First order logic with set theory (usually something close to ZFC but maybe with inaccessible cardinals and/or better support for proper classes)....
• 8,845
Accepted

### Learning Math Proof via Proof Assistants

I have a degree in software engineering and share the same goal as yours. Start with Informal Proofs Truth be told, you can learn more about proof by reading introductory maths book at university ...
• 350

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

As you found out, the usual technique to solve this kind of difficulty is to introduce a notion of "code" (what you called BotExpression), which expresses ...
• 5,146
Accepted

### Why are these two proofs so different?

There is a coq proof which doesn't require dependent induction: ...
• 291

### Comparison between proof assistants for coinductive structures and proofs

Here's my quick and dirty overview. I don't know Lean, so anyone who does is free to edit the answer to add it, but my impression is that co-induction isn't natively supported there yet. Coq: ...

### Why are these two proofs so different?

Additionally to the existing answer, there is also a way to use the same kind of pattern-matching facilities that Agda provides in Coq using the Equations library: ...
• 306
Accepted

### Do implementations of a PA and of ATP have overlap?

Unfortunately there is much less code reuse possible than one would hope. There three levels to consider: Differences between mathematical foundations (and implementations) between proof assistants. ...
Accepted

### Make ChatGPT write formal proof from natural language proof

This question can be interpreted many ways: Can ChatGPT produce valid Lean code if used naively? Can ChatGPT produce valid Lean code if used smartly? Can ChatGPT produce valid Lean code if hooked up ...
• 8,845
Accepted

### What is the best way to learn Iris completely independently

Specifically for Iris, one useful resource is the POPL'21 tutorial. It remains terse for a self-studying newcomer however. If you are not in a rush getting up to speed with Iris specifically, you may ...

### Is it possible to make a proof assistant program based on ZFC?

You could just add the ZFC axioms to Coq. I've done quite a bit of work in this system. ...
• 464

### Make ChatGPT write formal proof from natural language proof

Is this because ChatGPT is not good enough in Lean That is correct. Actually, it's not good enough at many things, for example, generating valid citations. ChatGPT is great at producing things that ...
Accepted

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

Your XY problem Let me step back and think about the XY of your problem. You have a category theory solver which already generates "proofs" and you want to export those proofs to be checked ...
• 8,845

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

You also asked about example projects which use proof assistants to reason internally in a topos. In the context of HoTT, Orton and Pitts have used (standard extensional) Agda to investigate ...

### Examples of theories where tactic language is required for simple proofs

so far I do not see any reasons why the same reasoning would not work for the rest of SF Wait for (or jump straight to) at least https://softwarefoundations.cis.upenn.edu/slf-current/Rules.html ;) 3. ...

### Are there minimal typed proof verifiers that can deal with the majority of mathematics?

It is hard to give an answer without knowing your use case. But it is fairly easy to make a minimalist HOL theorem prover. The axioms of HOL are quite simple. HOL-light is actually fairly ...
• 8,845

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

I find that Journal of Formalized Reasoning (Univ. Bologna) is covered by MathSciNet. I guess that journal ran from 2008 to 2020. LINK Also, Journal of Automated Reasoning (Springer) is covered by ...
• 131

### (Dis)Advantages of basing a proof assistant on CH correspondence?

Let us separate two things here: having dependent types, and using them to express logic a la propositions-as-types. As far as formalization of mathematics is concerned, there are no disadvantages to ...
• 9,553

### How do we know that we can trust proof assistance to produce correct results?

The completeness in Gödel's completeness theorem (yes there is one), is the property that you can prove everything that ought to be provable. Of course there is a precise definition of these. Dually, ...
• 4,015

### Comparison between proof assistants for coinductive structures and proofs

I do not know much about other proof assistants, but as for Coq I can say that there are quite some resources around that you might benefit from. Here is a starting point. However, the current ...
• 5,146

### Is there any formalization (with any theorem prover) of the Bohm theorem for lambda-calculus?

Not sure whether this answers your request, but Łukasz Czajka has formalized in Coq his proof of confluence (and normalization) of the infinitary λ-calculus modulo (strongly) meaningless terms. In the ...
• 229

### Which proof assistants implement Church's rule?

Not the answer you would like to hear, but that would be "no proof assistant" (to my knowledge). The first reason is that Church's rule does not hold for classical theories but the ...
• 9,553
Accepted

### Semantics verification of an LTL fragment logic

Simp rules for recursive definitions are supposed to be transparent, so you shouldn't need to invoke them for some simple applications. Tools like auto and ...
• 1,013

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

Here is a theoretical way you could do this in Lean 4. The key is that you can prove stuff about pure code in Lean. Lean's Declaration and ...
• 8,845

### Paths Between Quotient Types in Cubical Agda

I have comments inside the code. I am also interested if someone could further simplify the code. Also, keep in mind that your Int has two zeros, a positive one and a negative one. ...
Accepted

### are there any standard proof formats?

The OpenTheory system has a standard format for the core HOL logics supported by HOL Light, HOL4, ProofPower and HOL Zero.
• 1,102

### Are there minimal typed proof verifiers that can deal with the majority of mathematics?

Everything is almost trivial to implement if you strip it to bare bones. The Calculus of Constructions --- or more generally, pure type systems --- can be implemented in 100 lines of code, and if you ...
• 4,015
Accepted

### Which proof assistants implement Church's rule?

You might want to give a look at A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus by Yannick Forster and Fabian Kuntze. They define a set-up in Coq where using ...
• 5,146