This year several students have asked to formalize Mochizuki’s IUT
and abc proof in Lean for their PhDs. I warned them it’s academic career suicide
and urged them
to work on almost anything else. But some are carrying on anyway. What to do?