Skip to main content
16 votes

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 ...
Andrej Bauer's user avatar
  • 9,553
11 votes
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)....
Jason Rute's user avatar
  • 8,845
10 votes
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 ...
zacque's user avatar
  • 350
9 votes

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 ...
Meven Lennon-Bertrand's user avatar
8 votes
Accepted

Why are these two proofs so different?

There is a coq proof which doesn't require dependent induction: ...
tarzh's user avatar
  • 291
7 votes

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: ...
Joey Eremondi's user avatar
7 votes

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: ...
kyo dralliam's user avatar
6 votes
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. ...
Anja Petković Komel's user avatar
6 votes
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 ...
Jason Rute's user avatar
  • 8,845
6 votes
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 ...
Yannick Zakowski's user avatar
5 votes

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. ...
djao's user avatar
  • 464
5 votes

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 ...
Joey Eremondi's user avatar
5 votes
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 ...
Jason Rute's user avatar
  • 8,845
4 votes

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 ...
Maximilian Doré's user avatar
4 votes

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. ...
Alex Chichigin's user avatar
4 votes

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 ...
Jason Rute's user avatar
  • 8,845
3 votes

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 ...
Gerald Edgar's user avatar
3 votes

(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 ...
Andrej Bauer's user avatar
  • 9,553
3 votes

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, ...
Trebor's user avatar
  • 4,015
3 votes

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 ...
Meven Lennon-Bertrand's user avatar
3 votes

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 ...
sparusaurata's user avatar
3 votes

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 ...
Andrej Bauer's user avatar
  • 9,553
2 votes
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 ...
Pedro Sánchez Terraf's user avatar
2 votes

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 ...
Jason Rute's user avatar
  • 8,845
2 votes

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. ...
Apostolis Xekoukoulotakis's user avatar
2 votes
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.
Michael Norrish's user avatar
2 votes

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 ...
Trebor's user avatar
  • 4,015
2 votes
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 ...
Meven Lennon-Bertrand's user avatar
2 votes

Topic for undergraduate thesis

You profile says you're in applied math, so how about this: Define bipartite graphs as those that have a vertex 2-coloring. Prove that a graph is not bipartite if it has an odd closed walk (a self-...
Andrej Bauer's user avatar
  • 9,553
2 votes

Topic for undergraduate thesis

As others have said, your advisor is the best person to discuss this with. Having said that, I think another good place to go is the Lean Zulip. There you can have a back-and-forth discussion (not ...
Jason Rute's user avatar
  • 8,845

Only top scored, non community-wiki answers of a minimum length are eligible