>I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas
British mathematician Kevin Buzzard has been evangelizing proof assistants since 2017. I'll leave it to you to decide whether he is working on frontier research:
British mathematician Kevin Buzzard has been evangelizing proof assistants since 2017. I'll leave it to you to decide whether he is working on frontier research:
https://profiles.imperial.ac.uk/k.buzzard/publications