Bachelor thesis accomplished🎉

Stream: general

[Giacomo Maletto]

Hello, I'm a math student at University of Turin and I've been using proof assistants for about a year, with the objective of formalizing a computer science paper written by my advisor (about a class of functions similar in spirit to primitive recursive functions, but which are all invertible).

After a lot of work here's my thesis! https://github.com/GiacomoMaletto/RPP/blob/main/Tesi/main.pdf (Lean code in the same repo).
It's written in an informal, colloquial manner and I tried to turn it into an introduction/invitation to Lean.

Actually I've used Coq for 90% of the duration of the project, completed it, and then switched to Lean - doing basically the same thing in about 750 LOC instead of >3000. I'm not turning back.

Looking forward to start using Lean for something more involved!