Post B5Yb8LPzYm0bpN4foG by jonmsterling@mathstodon.xyz
 (DIR) More posts by jonmsterling@mathstodon.xyz
 (DIR) Post #B5Yb8K9IHN3dtIFp8y by jonmsterling@mathstodon.xyz
       1 likes, 0 repeats
       
       But one thing I am really concerned about is that there are not many constituencies involved in this discussion who are actually aware that "autoformalisation" of theorem statements / specifications can easily produce vacuous specifications, and that as AI capabilities increase, it will be more and more difficult for humans (and AIs) to tell whether the autoformalised specification has anything to do with the mathematical problem at hand. In this hypothetical world, refereeing goes from a straightforward "spot-check the math, assuming good faith on the part of the author/mechaniser" process to a true needle-in-haystack scenario. Mechanisation, far from increasing confidence in the results, will decrease the level of confidence that we may justifiably have in mathematical results.I am really concerned when I see professional mathematicians telling me that they are excited that the system will be able to translate their precise English specification into a formalised theorem statement, so that they don't have to understand the code. That is the one part that LLMs will never EVER be able to do with the reliability required by mathematics.  The LLM can certainly in many cases fill in the proof, which is cool.  But professional mathematicians are always shocked when I tell them that no version of the current AI technology will EVER be able to translate their specification from English into Lean in a way that would not require them to be a Lean expert.
       
 (DIR) Post #B5Yb8L1X1iRWbVd8gS by jonmsterling@mathstodon.xyz
       0 likes, 0 repeats
       
       Mathematics has never ever been adversarial until now. The fact that mathematicians may freely assume good faith of all their fellows is what has made the review of both non-mechanised and mechanised mathematics tractable."Autoformalisation" is a buzzword for a new kind of mathematics that is inherently adversarial. Whether a result is a theorem or an "exploit" (hahaha) will take immense amounts of energy to determine.I don't think that people are really understanding how absolutely crucial the non-adversarial nature of mathematics has been, and how the loss of the good-faith assumption could actually lead to mathematics being set back hundreds or even thousands of years. It's existential.
       
 (DIR) Post #B5Yb8LPzYm0bpN4foG by jonmsterling@mathstodon.xyz
       0 likes, 0 repeats
       
       By the way, if you don’t believe me, consider that that grifters have raised tens of millions USD in venture capital off of a faked solution to an Erdos problem (I say faked because what it solved was trivial and not an actual Erdos problem). That is what I would call an “exploit”.