Eric Astor

Stream: new members

[Eric Astor]

Hi all - Eric here, software engineer (and former logician) starting to get interested in all of this. In my previous life, I did reverse mathematics & computability... I've noticed there's already some solid computability in mathlib, maybe with some opportunities for expanding to newer results. Anyone know if it might be feasible to formalize reverse math in Lean?

[Jia Ming]

Idk what to say but I also heard the phrase "reverse mathematics" from the 2nd presentation (about Church's Thesis & other axioms in Coq) of this conference session: https://www.youtube.com/watch?v=myMM7FuaJY4&t=1638