Some good things about Anthropic/OpenAI/Lean

It is a powerful wake-up call to the necessity of adopting a strictly intuitionistic and constructivist logical and philosophical foundational framework for mathematics. We must thus completely reject the Lean 4 libraries (Mathlib) which are essentially dependent on non-constructive axioms.

Also an incentive to examine critically the theoretical (soundness) and implementation aspects of the underlying type system of Lean 4.

Furthermore, Anthropic/OpenAI/Lean is a wake-up call to the importance not only of constructivism but of feasibility and bounds. Much ado is made about incompleteness results. We now need to bring into the spotlight results about the non-feasibility of certain mathematical proofs, algorithms or values. A shift of focus from what computers theoretically can or cannot do to what computers can effectively do and not do. Give a million examples of meaningful mathematical statements which, from the standpoint of a certain metatheoretic framework, current computers effectively cannot process.

Finally, Anthropic/OpenAI/Lean has provided powerful argumentation for rejecting the formal mathematics project in favor of adopting a new discipline for human mathematical writing (and reviewing). All human written proofs can, with some hard work and time, be made clear and accessible so as to render superfluous the original motivations for formalizing mathematics using proof assistants. This new discipline will guarantee transparency, trust and readability and can itself be integrated into a new form of software which is not a proof-assistant but rather something that could be described as a semantic extension of LaTeX.

In fact, once generative AI is cast in the dustbin where it belongs, a new technology and type of software may open up a whole new future for humanity. I still believe that the primary purpose of computers was, and can still be, to enhance human intelligence and creativity and to redirect human attention away from material conflicts. The tired old myth of "artificial intelligence" has to go. Instead, the computer is to assume the role of a tool and companion for "Mentats" (or rather the ancient philosophical ideals of intellectual cultivation and wisdom).