Hello all! I am really new to proof assistants and Zulip, so I apologize if I don't have any idea about what I am asking, or if I'm in the wrong stream.

TL:DR: Suppose I want to try to formalize reverse mathematics in Coq as a project. Is this sane?

I'm in my third year of my undergraduate mathematics degree and I am starting to think about projects to do for a bachelor's thesis. I am especially interested in reverse mathematics, but a general theme in computability theory is that the proofs are given in a kind of "procedural" style, where you give a sort of recipe to construct a set in an attempt to convince the reader something is true. I figure it would be nice to be able to formalize proofs about classical reverse mathematics in a proof assistant, say Coq, but I am not sure if this works because I can't seem to find any such work online.

My "plan" is to somehow formalize RCA_0 in Coq, somehow have the ability to add extra axioms to state and prove certain classic analysis theorems (e.g. Heine Borel), and do the reverse part by proving the additional axioms assuming the theorem. I think this would make a passable project if I do succeed...

Normally for such questions, it would be wise to approach a faculty member in my university to ask, but I don't think any of the faculty in my university works with proof assistants (not that I know of). I know a professor who works with reverse mathematics but I don't believe he has experience with proof assistants. A quick google search reveals that there was a seminar a decade ago that did this, but unfortunately I did not find any materials related to the seminar at all, despite heavy googling.

Hence this post. I want to know if what I'm suggesting is sane for an undergraduate to do as a project, and if it is, is there any resources I can look at. Thank you!

I recommend taking a look at previous work on reverse math in Coq like this one: https://arxiv.org/abs/2009.00416 https://github.com/uds-psl/churchs-thesis-coq

cc: @Yannick Forster who may be able to link more previous work on rev math in Coq.

I will take a look at it. Thank you!

Hello, always happy to see reverse mathematics questions pop up here! :) Thanks for the ping Karl

First, let me mention that there are two related but relatively separate areas of reverse mathematics: Classical Reverse mathematics á la Friedman, with the important book by Simpson. Here everything is based on RCA_0, a logic which allows the law of excluded middle, i.e. classical proofs, but has almost no set comprehension principles. The central question then is how strong comprehension principles need to be to prove certain results, e.g. the mentioned Heine Borel theorem

And then there is Constructive Reverse Mathematics à la Ishihara: Here one works in a Bishop style constructive logic with arbitrary comprehension principles but no classical principles such as the law of excluded middle, and then asks similar questions

With Dominik Kirst and other colleagues, I have worked on constructive reverse mathematics questions for computability theory and for first-order logic

The relevant papers are linked here https://github.com/uds-psl/coq-synthetic-computability/ and here https://github.com/uds-psl/coq-library-fol

I would say that a RCA_0 proof of Heine Borel in Coq would make up for very exciting work, but I would expect it to be very, very, very challenging, to the point where my first gut feeling is that it is too challenging - not even just from the perspective of being a Bachelors' thesis topic, but even from the perspective of being a machine-checkable result

The reason is that one has to formalize RCA_0, and then carry out all proofs in this logic, meaning that results in libraries of Coq proofs or Coq tactics become useless - one has to construct derivations for everything explicitly, which creates a huge overhead

But: @saddle196883 you can drop me an email at yannick.forster@inria.fr and maybe it makes sense to chat via Zoom a bit? I don't know whether I can really help in the end with finding a suitable topic in this area, but I can try :)

on the other hand, there has been work on "proof modes" for reasoning inside a logic embedded in Coq using tactics. The most famous is the Iris proof mode. However, proof modes are in my view definitely not bachelor level material.

Also, I'd have to recommend bachelor-level projects that do some small well-defined contribution to an existing Coq library over making new projects from scratch

Yannick Forster said:

But: saddle196883 you can drop me an email at yannick.forster@inria.fr and maybe it makes sense to chat via Zoom a bit? I don't know whether I can really help in the end with finding a suitable topic in this area, but I can try :)

Sure! I am writing an email now.

Karl Palmskog said:

Also, I'd have to recommend bachelor-level projects that do some small well-defined contribution to an existing Coq library over making new projects from scratch

This sounds like a good idea, but if no one in my faculty does Coq related work, I am not sure if they are willing to supervise such a project. I will certainly try asking around though.

I was hinting at that Yannick might point to a project that performs some extension on top of the UDS-PSL Coq libraries, but he may already have thoughts in that direction. Just saying that something like this would likely have a much higher chance of success than a "new" project.

Mark Koch indeed implemented a FOL proof mode, heavily inspired by Iris, as part of the uds-psl FOL library: https://coq-workshop.gitlab.io/2021/slides/Coq2021-02-01-slides-fol-toolbox.pdf And I agree, maybe we can find something that extends previous work by Dominik and colleagues rather than starting from scratch

In addition to all the great info here, Lawrence Paulson paper about the formalization of Gödel's 2nd incompleteness theorem has a great writeup of the challenges of working in a "reductionist" setting, in his case HF sets .

Last updated: Jun 18 2024 at 22:01 UTC