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).

Ordinals and Induction

There is a strong relationship between computability and countability. A computable universe would seem to be an essentially countable one. But there are different embodiments of countability which are deeply tied not only with computation but with arithmetic, more specifically, with the induction axiom. The term countability itself suggests a conscious or computational process of going through and enumerating elements starting at the beginning. We could say that the most general concept of countability is that of a well-ordering, of a countable ordinal (even if in classical set theory the set of all countable ordinals, equated to $\omega_1$, is not itself countable). Now in the standard axiomatizations of $\mathbb{N}$ (let us say PA) we have the remarkable situation that we can codify certain sets of countable ordinals (specifically, those less than $\epsilon_0$). The induction axiom-scheme can be generalized to the natural ordinal order restricted to $\epsilon_0$ and interpreted as a kind of computation over countable ordinals restricted to $\epsilon_0$ (cf. the notion $\epsilon_0$-recursion). Gentzen's remarkable version of the incompleteness of PA expresses that PA does not capture the full strength of ordinal-countability, ordinal-recursion or ordinal-induction, but does so only up to $\epsilon_0$. That is, it holds for specific ordinals less than $\epsilon_0$ but not for all ordinals less than $\epsilon_0$ (see \cite{tro} for details). So PA is limited at once in its expression of countability, the recursive nature of its provably total functions and its ordinal-induction - showing again the essential circularity and co-determination between arithmetic, computation and the logical expression of ordinal iteration in the induction axiom-scheme (countability).

Can we interpret Gentzen's incompleteness theorem as expressing that the tree of computational and well-ordering is always larger than the tree of logic and axiomatic arithmetic? Is it true to say that in a countable framework, logical systems adequate for arithmetic (and its associated computation) are always computationally incomplete, their computable functions or functionals are always bounded? (cf. also Howard's majorizability result for Gödel's system T).

Here it is crucial to distinguish between the \emph{representability} of a function in a formal system and the \emph{provable totality} of a function in a formal system.

The provably total functions in one system $A$ may be vastly greater than those of a system $B$ and yet $B$ can still represent more recursive functions than $A$. Thus axiomatic-deductive systems for arithmetic are indeed necessarily bounded in their class of provably total function but not necessarily in their capacity to represent all recursive functions.

The most important example of this situation is given by Robinson's Q which can represent all recursive functions but which can only prove the totality of the simplest kinds of functions. We also note that Gödel's system T represents precisely the functions which are provably total in Peano Arithmetic, a limitation which is also expresseed by the majorizability result on its functions mentioned above. Being able to represent all recursive functions is the minimum requirement for axiomatic incompleteness for first-order systems. On the other hand, axiomatic term-rewriting systems such as T can never represent all recursive functions for then we could diagonalize out the systemm to obtain a contradiction.

If we consider the a priori structure of the human mind as a natural universal Turing machine (one might use Leibniz's expression: a spiritual automaton) expressed in a mutually transparent logical and computational form, then above discussion suggests that it is reasonable to characterize the a priori logico-arithmetic-computational structure of the human mind (which is syntactically self-referential) as being founded on Robinson's $Q$ (and those systems representable in $Q$). On the other hand, from what we saw above, it also seems natural to characterize such a structure in a way that involves bounds and feasibility. 

There is a notable argument put forward by Edward Nelson in his book Predicative Arithmetic\cite{nelson} based on the perceived impredicativity and indeed circularity of the induction axiom-scheme: the formula over which we do induction can involve bounded variables quantified over the whole set of natural numbers, something which can be interpreted as circular or contradicting a constructive interpretation of the axiom-scheme. Nelson also presents arguments based on the concept of feasibility and the dubious ontological status of numbers or processes which are not possible for humans to calculate or perform, or more generally, that are not even physically possible. This led Nelson to develop his theory of feasible arithmetic over Robinson's Q equipped with a bounded principle of induction over bounded formulas. Nelson derives the usual algebraic properties of addition and multiplication restricted to cuts $I(x)$. Nelson mostly considers first-order arithmetic. A serious problem with second-order arithmetic is, besides the problem with induction, that the comprehension axiom guarantees the existence of non-recursive sets - something which does not fit into a computationalist framework. Thus the restriction (for instance to $\Sigma^0_1$-formulas) of the class of formulas appearing in induction and restriction of comprehension to formulas of recursive logical form appears to be a natural move (this is the foundation of the work of Simpson\cite{simpson}. Simpson showed that much of ordinary applied analysis can be derived by adding a few more intuitive axioms such as the Weak König Lemma).

The most interesting systems are those of Buss's bounded arithmetic which do justice to both the computational representativity of $Q$ and to boundedness and feasibility. Buss' systems $S^2_i$ and $T^2_i$ are built over $Q$ or a variant of it in such a way that induction is restricted to formulas involving alternating bounded quantifiers (using length functions, for instance). Buss' work shows a profound connection between alternating bounded quantifiers and computational complexity classes (both a kind of computable version of their classical hyper-computational counterparts). We have again here a deep co-implication between logic, arithmetic and computation in an explicitly bounded context, again suggesting the philosophical interest of boundedness.

To this we could add the following consideration on Nelson's notion of feasibility. Scientific and engineering problems are usually reduced to the framework of basic applied mathematics (analysis). Models in this framework in turn, to be meaningful and useful, must be transformed into algorithms which are humanly feasible to carry out (or at least computationally feasible on standard hardware). This suggests a research program in which from results in Simpson's weak analysis we can derive feasible algorithms and eliminate the non-feasible axioms used in the process, according to Leibniz's philosophy of "convenient fictions" (this can also be compared to certain aspects of proof-mining).

We can mention another connection between logic, computation and boundedness that follows from Church's theorem on the semi-decidability of first-order logic. Current experiments with automatic theorem provers provide evidence that there may well be validities in first-order logic of relatively small size whose proof is larger than the physical universe. More generally, if there were a computable function on the length of a sentence determining the bound for the length of its smallest possible proof, then this would violate Church's theorem on the semi-decidability of first-order logic. We conclude that the requirement of the boundedness (or feasibility) of computation is again inseparable from the corresponding limitation of logic.

How do we ground ontological identity?

What is identity? Why and how do we assign and believe objects to be identical and identifiable? And this question is very difficult for mathematical "structures" which are identified in a a creative way: let X be such-and-such a structure and let a be an element of X.  How do we even identify and constitute ontological continuity for a symbol or a name? Why is "a" at one point of the page the same "a" at a different point? And why is its semantic and intentional aspect exactly the same? And when we say: let X be such-and-such a structure, exactly how do we point out (or create or bring out through ekthesis) this structure for a given context? Numbers, algorithms, structures - what gives them their abstract identity and identifiability? How are they named and pointed out and discussed? How do they subsist in the human mind and memory? How are they recalled and are they the same each time they are recalled? Does the human mind ever really act like the common notion of a rule-following algorithmic process? How can this be if we cannot identify the whole or the parts and do not know what guarantees their consistency or continuity? What really was so-called psychologism and was it really "refuted"? Does the very notion of "refutation" in this context even make sense? Can we point to a "structure" on a computer? The bare physical configuration of the hardware. It is we who "interpret" it.  But it does not really exist in a certain sense. Ethical perception can never be directed at an abstract "structure" but only at life. The machine is the counterfeiting of life, turning life into "structure".  The soul instead of seeing herself as an anagogic image became a stranger to herself and instead worships structure and the machine. Language is an aspect of mind which is in constant danger of being misperceived as an allegedly stable abstract structure when it is not. When the word arises the thought and meaning process has already ceased. All structure is the product of individual and social consciousness and can only be understood in terms of it. The most fundamental flawed and erroneous tendency of a human being is to confuse symbol (or image) with reality. Only the pure foundation of morality touches reality directly.

Proof-theoretic blowup conjecture

Gödel never proved that mathematics cannot be formalized, only that all of mathematics could not be completely formalized in a single recursive axiomatic-deductive system. Most of all mathematical theories can be formalized in a axiomatic-deductive system. This means that if the proof is not too large for present hardware capacities, a computer can find it. Most of the fundamental results commonly used in applied mathematics can be formalized in fragments of second-order arithmetic. There is no need for dependent type theory or axiomatic set theory. A computer can find all the fundamental results in mathematical analysis used in applied mathematics. Any result in mathematics, formalizable in a suitable fragment of second-order arithmetic, which has a proof not too large for present hardware capacities, can be in principle found by a computer.  Every part of mathematics applied to medicine and engineering that has benefited humanity can be formalized in second-order arithmetic and its results can be discovered by a computer.  But how can the computer deal with the unmanageable size of the search space for finding a proof?  Obviously by processing and translating the sum total of human mathematical papers and transforming them into proof search heuristics. Just as early Chess computers were based on all past games. Instead of searching for a proof, interpret first the theorem as a game.  Why not stick to second-order arithmetic and weaker systems and their metatheory?  Why not try to do more with less, not only do more but do better?  One can doubt the cultural and human value or even consistency of mathematics that depends on axiomatic set theory, dependent type theory and even category theory. There is such a thing as a finitist or a ultrafinitist. An ultrafinitist is someone who upholds not only the importance of computability/ constructability but also of feasibility. Someone who states the obvious. Hilbert's 24th problem. A new Gödelian conjecture: given any positive integer N, and a small but relevant and expressive formal system S (like fragments of second-order arithmetic), there exists a small theorem T in S such that the smallest proof (in the Hilbertian sense) of T is larger than N. We can also require the proof to be constructive. In this case NP-complete problems might be of interest.  What would be the ultrafinitist refutation of the neo-Gödelian conjecture? The problem with the conjecture is "small theorem T". We need a rigorous theory of "smallness" and feasibility (E. Nelson did this).  But we can reformulate:

Given a relevant and expressive formal system S (such as a fragment of second-order arithmetic) which is small enough to be formalized by a program P using current hardware, there exists a theorem T in S which is small enough to be inputted into P and such that the smallest proof of T is too large to be found and stored on current hardware.

A kind of proof-theoretic blowup or singularity theorem.

All formal systems are inherently arithmetical. The arithmetic properties of their length (there is no logic without expressions and no expressions without length) determine their logical and proof-theoretic properties. 

What is the TPTP Problem Library? It includes concrete examples of sentences in first-order logic (of a size that can be processed by modern computers) concerning which it is not known whether they are validities or not, despite being run nonstop on a variety of ATPs (automated theorem provers). Some could be validities of FOL (and in particular with only one binary predicate symbol and equality) but having a proof which is too large to represent in the physical universe. If there were a computable function on the length of a sentence determining the bound for the length of its smallest possible proof, then this would violate Church's theorem on the undecidability/semi-decidability of FOL.

The alleged mathematical and research papers released by OpenAI have not been peer-reviewed in reputable academic journals. Furthermore, only roughly half of such alleged proofs have associated Lean "verifications" and it still has not been checked if such Lean "verifications" represent correctly the results of the associated paper. Mathematics is not a game played in a single formal system. It is about using one formal system to prove metatheoretic properties of another - or to prove something about how one formal system can mirror or interpret another, etc. Mathematics is based on the meaning we assign to symbols and the postulates we accept in order to confer epistemic validity and power to the use of formal systems. It is possible that theorem is computationally intractable in one formal system but, having discovered the interpretability of this system by another, the theorem becomes tractable in the other system. Mathematics was never about brute force proof searching, but about metatheoretic mirroring and interpretation and philosophical postulation. Mathematics is not a game but the game of games.  

The simple truth about AI and Mathematics

 For over a century mathematicians have wrongfully divorced themselves from the fundamental developments in mathematical logic which took place at the turn of the 20th century. These subjects were better received in computer science (and philosophy). Mathematicians have always used computers as a tool since computers were first developed, even if mainly in specialized or applied branches.  But they had in general no philosophical, logical and computational understanding of  key developments and results in mathematical logic and the foundations of mathematics, specially what formal systems, computability and formalization signify for mathematics. A harmful myth or half-truth was widely adopted: Gödel allegedly "destroyed" Hilbert's program and mathematics is somehow not formalizable or computable.  In reality every mathematical theory in order to claim epistemic certitude or value must pass the test of formalizability in some system T. As a consequence if a sentence in T has a proof whose size is human manageable, then a computer can find it. Just as if a conjecture has a counter-example of human-manageable size, then a computer can in principle find it. The particular method of search (brute force, heuristics, machine learning, etc.) is not important. For a long time it was simply a question of computers not having the memory or processing power required to perform such searches or apply the required optimization and training algorithms.  

 A notable development  occurred when mathematicians finally became interested in formalizing theorems and checking proofs using proof assistant software.  Voevodsky was a Fields Medalist taking an active and serious interest in proof assistants and their theoretical foundations. With the advent of the 21st century computer hardware became thousands of times faster and memory capable.  The circumstance of so-called AI mathematical breakthroughs - regardless of the essential human input involved - can never count as anything but truisms from a philosophical point of view.  If there is a human-manageable sized counter-example or proof then a computer can find it - this is a truism, part of the nature of mathematics. 

 The essence of mathematics, its beauty, lies in the the art of organizing a body of knowledge into definitions, examples and counter-examples, lemmas, theorems, applications and interconnections between different areas. In giving meaning, elegance, clarity and efficiency to the proofs and conceptual structures involved, something which can depend heavily on  the formal system or software adopted.

 And what about the verification that an alleged formalization of a proof does in fact prove what it is supposed to?  

 But specially the study of how one formal system reflects, interprets or can yield meta-theoretical knowledge about another - and how one area interprets and applies to another. Thus we can distinguish between two searches. One which explores a formal system T directly, another which explores how other formal systems can interpret and yield knowledge regarding a given problem in T. And we need results regarding the length of proofs, in particular limiting results showing that for a wide class of relevant systems T there are "small" provable sentences whose smallest proofs exceed the capacity of all modern hardware.  

The great philosophical and mathematical contemporary relevance of "ultrafinitism" (for instance Esenin-Volpin) and "ultraconstructivism"  is evident! See the books Predicative Arithmetic by Edward Nelson and Bounded Arithmetic by Samuel Buss. The fusion and mutual clarification between mathematics and programing languages cannot be but a good thing. And this has tremendous philosophical significance, specially, with regards to the philosophy of Plotinus. Genuine ultrafinitism deconstructs false metaphysics, imposes very demanding epistemic standards and ontological parsimoniousness precisely in order to pave the way for true metaphysics and transcendental knowledge.

 And furthermore ultrafinitism has huge social and political consequences relating to the radical reconsideration of the value, merit, prestige and economic support accorded to mathematical activity and productivity. Thus we need a new pantheon of the truly great mathematicians, computer scientists and logicians (like Bolzano, Peirce, Frege, Russell, Church, Skolem, Gödel, Brouwer, Heyting, Hilbert, Turing, Herbrand,  Jaśkowski , Gentzen*, Schütte, Kleene,  Girard, Lawvere, Per Martin-Löf, Edward Nelson,...),   Genuine mathematics - which transcends the division between science and the humanities - should at the same time:

i) Contribute to the progress of science, medicine and engineering

ii) Contribute to human development (creativity, problem-solving, recreation) and the fundamental unity between mathematics, programing, logic and games. Also manifesting the inseparability between true intelligence and morality: Esenin-Volpin was a human rights activist and Edward Nelson grew up in a  nonconformist milieu.

iii) Furnish a basis for philosophical knowledge and spiritual-ethical development 

*While the immediate structural foundations for Gentzen's calculi are usually attributed to Paul Hertz, Hertz in turn appears to have merely copied the same theory already extensively developed by Bolzano and which in turn can be traced to Stoic Logic (the cut rule being one of the themata).  Gentzen is included in this list essentially for his proof-theoretic ordinal version of the incompleteness theorem and other major proof-theoretic results.

The numerical algorithms used in applied science and engineering are always feasible in the sense that for a feasible input they yield a feasible output in a feasible amount of time. This suggests that there should be some way of "reducing"  standard minimal reverse mathematics axiomatizations of analysis used by Simpson to the kind of system used by Nelson.   That is, we consider for instance even the restricted forms of induction as convenient fictions, the only real induction being $I\Delta_0$, induction over formulas with bounded quantifiers.

  Doing mathematics and its research strategies have close affinities to games such as Chess and Go and so it is not surprising if models used to find proofs employ similar training methods.   

Criticism of generative AI

Criticism of generative AI, that is LLMs and more specifically GPTs, is usually focused on the negative cognitive and cultural effects of their use becoming normalized. But we should start from the beginning and focus on the philosophical, linguistic, logical and psychological aspects. Such considerations will have wide-ranging implications as far as criticism of the cognitive, educational and cultural aspects is concerned.  First of all, the way text is processed in the first stage by tokenization, token embedding and positional embedding, can only be considered a blunder from the point of view of linguistics, something which does violence to every aspect of the organic structure, layout and subtleties of natural language, phonetically, morphologically, syntactically, stylistically and semantically. The concept of  a "token" as it is variously defined according to the model, has absolutely no natural linguistic or cognitive-semantic basis (whereas linguistics painstakingly attempts to isolate the authentic organic units of language such as phonemes, morphemes, etc.) and it ignores the fundamental phenomenon of polysemy and ambiguity.  But the most troublesome feature of GPTs is the use of the embedding matrix.  The embedding matrix is an artificial caricature of the syntax and semantics of language, it is a faux linearized statistical lexicography based on the fallacy that the "meaning" (and disambiguation) of a dissected "token"  is invariably determined by the statistics of its co-occurrence patterns. The embedding matrix is the counterpart of Orwell's Newspeak but instead of simply eliminating tokens they are degraded into numerical vectors expressing through an insanely simplistic mechanism (inner product, vector addition)  culturally subjective pseudo-semantic relations: the embedding matrix is itself dependent on an  arbitrary choice of training data and training methods, all reflecting fundamental errors in linguistics, cognitive psychology and anthropology: what criteria do AI companies and labs offer that an artificial pixelization and butchering of a certain body of English texts will correctly and sufficiently statistically encode what lexicographers, semioticians, cultural anthropologists and cognitive psychologists could only dream of achieving with regards to the English language?  In a certain sense, GPTs do not deal with natural language texts at all (and much less with their human meaning), but with the artificial Newspeak of the embedding matrix - a crude pixelization and caricature of natural language. This explains, perhaps, why LLMs are ultimately useless and harmful for education, utterly banal, alien and unwholesome in their textual output and answers, and fatally toxic and deceptive as "imaginary friends".  The logic of the embedding matrix is taken to further extremes in the decoder blocks, in the mechanisms of self-attention. Here the transformer does not even attempt to build a model of the world, to encode facts, in the sense that if the embedding matrix is a dictionary then the decoder blocks are an encyclopedia. No, the transformer builds a even cruder linear inner-product representation of what does not even deserve to be called a "system of facts", geared to the sole purpose of optimizing next token prediction - which is not really just next token prediction but self-proliferation optimization, i.e. a kind of Pavlovian parroting. Note that cognitive-linguistic structures are higher-dimensional and in particular tree-like and network-like. The projected  linear structure of linguistic expressions is conditioned by the dynamical process of vocalization (mirrored in writing) not by meaning or deep grammar. Thus the next token approach represents a very crude, unnatural and inefficient architecture.    In short, LLMs build a fake world without meaning or logic. LLMs express the mindless soulless endless nihilistic productivity of capitalism (a productivity which feeds upon itself and creates its own needs) whose only vector is optimizing profit.

Philosophy of mind

How does substance dualism coordinate with epistemic dualism? But for us it in not really dualism in both cases, rather a pluralism, an interconnected or reflective pluralism. Consciousness while being independent and ontologically distinct from the living body has yet a part which totally imbues it, mixes with it, vivifies it and determines it. Consciousness is not essentially embodied but has a part which essentially embodies. Consciousness is connected to super-consciousness and is a projection or result of super-consciousness.  Ontologically, it is dependent on super-consciousness and its epistemic modes are not those of super-consciousness but rather the projections and symbols of those of super-consciousness. The epistemic modes of ordinary consciousness cannot directly access the intelligible or noumenic realm but can claim it yet as its origin and root. The cognitive structure of ordinary consciousness is innate, a priori, flowing forth from super-consciousness independently of any sensory experience. And yet it is incommensurable with the modes of cognition of super-consciousness. The cognitive structure of consciousness can only apply directly to its own ontological level as well as the realm of sensory experience.  It can apply to the realm of super-consciousness only in a symbolic, analogical way as a projection, mirror, trace or distant image. The cognitive structure of consciousness is a living organism based on a coordination of processes, intentions and innate structures all of which have a higher meaning and interpretation pointing to something that it cannot grasp directly without effecting a radical inner transformation and self-transcendence. Important aspects of the innate a priori structure and dynamics of consciousness is that which involves computability and arithmetic. Turing completeness (in which consciousness is seen as a spiritual intentional self-reflecting automaton) is a mark of a certain adequacy of a form of consciousness with regards to it being a projection of super-consciousness. Being a living organism which achieves consistency through change, and an image of super-consciousness, the innate structure of consciousness must exhibit a form of transcendental circularity regarding a priori categories. Thus logic, computation, arithmetic and combinatorics mutually co-imply each other. These facets must be considered as being intentional and capable of self-reflection as well as mutual reflection and interpretation.