Not sure every mathematician would be happy to do this... it sounds much less pleasant than thinking. It's like saying mathematicians would rather be programmers lol. It's a significant difficult problem which i believe should be left completely to AI. Human formalization should become dead