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 and the general trend was to use them as a tool in certain 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' 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.
But 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. 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.
No comments:
Post a Comment