Formalizing Kleene tree (computability)

Stream: mathlib4

[Thomas C.]

Hi everyone!

I wanted to share my first real project written in Lean and have your feedback.

The Kleene tree (as described in this paper) is an infinite, computable, binary tree which has no computable path.

It is used in computability and in reverse mathematics (in particular, to show that the system WKL0 is stronger than RCA0) and I thought it was a good start for me as some required computability theorems were already proven in Mathlib.

Here is the code: https://github.com/tchaumeny/KleeneTree

I would very much appreciate any feedback regarding the choices I made and the way the code is written.