I found there’re few types of response of internet for OpenAI’s work on formal math & theorem proving/discovery recently. 90% of my Twitter’s feed is about OpenAI’s bombshell.
Personally, I’m not pissed off as math-guy. It’s a mix of feelings: a bit surprise that Lean actually does the job and math being cracked this way, a bit disappointed about myself and even came early with right prediction about future but couldn’t help it, a bit thrilled (and scared at the same time) for living this era. I see few redditors said they wish they were born 30 years earlier.
There’s lot of work to do, the future of humanity will be on the Mars and other planets, Math before 2026 is like programming/computers of 1970s, belong to small group of people, but from now on, It will be commoditized, like PC-for-everyone moments of Apple & Microsoft in 1970-80s.
Math still keeps involving, developing, becoming tool for science, but the work will be different: more frameworks, more layers, more ways to work on, must be even cheaper and It’ll 100% be cheaper.
People are still debating OpenAI were right or wrong. It doesn’t even matter at all, or It matters in a different way. All we know is one powerful thing exists. Nuclear bomb exists. It might be right or wrong, but It exists, despite of It should or should not. It’ll never be earased. It’s one-way. It can’t be reversed. Same, we know that one power of doing math that way, exists, whether It should or shouldn’t. And It can’t be reversed.