Zulip Chat Archive

Stream: new members

Topic: Eric Astor

view this post on Zulip Eric Astor (Jan 28 2021 at 05:49):

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?

view this post on Zulip Jia Ming (Jan 31 2021 at 21:57):

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

Last updated: May 11 2021 at 22:14 UTC