He seems genuinely interested in Surreal numbers. Seems like he found value in exploring them and the Lean process, devoting time and interest to it and understanding what it's like to be a mathematician. I think a lot of people who go into Computer Science may have been mathematicians in the 30s before they became separate majors at the university level.