How feasible it for me to translate this real analysis video

Stream: new members

[Adamthecoder]

Real Analysis | The countability of the rational numbers. | Michael Penn

https://www.youtube.com/watch?v=ja94Pn89i3I

I'm an experienced C++ programmer, familiar with some formal mathematics (0th-2nd order logic, ZFC, and PA), and I'm learning real analysis. I thought it would be interesting to translate my pen-and-paper math into a program that demonstrates the proof (since, thanks to Curry-Howard, programming = proofs).

Am I still too early for this? Is Lean4 a reasonable language to use for this purpose? Will this complex real analysis proof take months to complete solo?

It seems that Lean4 proofs are quite verbose, and maybe trying to translate pen-and-paper proofs to programs is a mistake...

[Riccardo Brasca]

Translating proofs to program is the whole goal of formalization, isn't it? For example the theorem you want is docs#Rat.instEncodable (of course you can try to reprove it by yourself!).

[Riccardo Brasca]

On how difficult it is, it really depends on which proof you want to formalize (I have to admit I didn't watch the video), but if you have a precise pen and paper proof it is a good way to learn some Lean!

[Maxim Kalentsov]

From my very limited experience with Lean 4, formalizing this proof seems reasonable - I am sure it is possible to write the whole proof in a few hours, if one is fluent with syntax. Learning said syntax may take some time, but I don't think it will be too long, and you probably won't need much more than learning resourses from documentation page.