The cultural divide between mathematics and AI

If you look closely at the history of mathematics you can see that it worked similarly to current AI in many respects (not so much the secrecy) - people were oftentimes just concerned with whether something worked rather than why it worked (eg so that they could build a building or compute something), and the full theoretical understanding of something sometimes came significantly later than the knowledge of whether something was true or useful.

In fact, the modern practice (the concept predates the practice of course, but was more of an opinion than a ritual) of mathematics as this ultimate understandable system of truth and elegance seemingly began in Ancient Greece with their practice of proofs and early development of mathematical "frameworks". It didn't reach its current level of rigor and sophistication until 100-150 years ago when Formalism became the dominant school of thought (https://en.wikipedia.org/wiki/Formalism_(philosophy_of_mathe...), spearheaded by a group of mathematicians who held even deeper beliefs that are often referred to as Mathematical Platonism (https://en.wikipedia.org/wiki/Mathematical_Platonism). (Note that these wikipedia articles are not amazing explanations of the concepts, how they relate to realism, or developed historically but they are adequate primers)

Of course, Godel proved that truths exists outside of these formal systems (only a couple decades after mathemticians had started building a secret religion around worshipping Logos. These beliefs were pervasive see eg Einsteins concept of God as a clockmaker or Erdos' references to "The Book"), which leaves us almost back where we started where we might need to consider there may be some empirical results and patterns which "work" but we do not fully understand - we may never understand them. Personally, I think this philosophically justifies not subjecting oneself to the burden of spending excess time understanding or proving things that have never been understood before - it may elude elegance (as the 4-color proof) or even knowability.

We can always look backwards and explain things later, and of course, it's a false dichotomy that some theorems or results must be fully understood and proven (or proven elegantly) before they can be considered true and used as a basis for further results. Perhaps it is unsatisfying to those who wish to truly understand the universe in terms of mathematical elegance, but that asshole used mathematical elegance to disprove mathematical elegance as a perfect tool for understanding the universe already, so take it up with him.

Personally, as someone who at one time heavily considered pursuing a life in mathematics in part because of its ability to answer deep truths, I think Godel set us free: to understand or know things, we cannot rely solely on mathematics. Formal mathematics itself tells us that there are things we can only understand by discovering them, building them, or experimenting with them. There are truths that Cuda Cowboys can uncover that LaTex Liturgy cannot

The nature does not care whether it fits in our brains.

It would be like having the machine code to something amazing but lacking the ability to adequately explain it or modify it - the machine code is too big and complicated to follow, so unless you can express it or understand it in a better way, it can only be used exactly how it is already.

In mathematics it is just as (if not moreso) important to be able to apply techniques used to solve novel proofs as it is to have the knowledge that the theorem itself is true. Not only might those techniques be used to solve similar problems that the theorem alone cannot, but it might even uncover wholly new mathematical concepts that lead you to mathematics that you previously could not even conceive of.

Machine proofs in their current form are basically huge searches/brute forces from some initial statements to the theorem being proved, by way of logical inference. Mathematics is in some ways the opposite of this: it's about understanding why something is true, not solely whether it is true. Machine proofs give you a path from A to B but that path could be understandable-but-not-generalizable (a brute force), not-generalizable-but-understandable (finding some simple application of existing theorems to get the result that mathematicians simply missed), or neither understandable-nor-generalizable (imagine gigabytes of pure propositional logic on variables with names like n098fne09 and awbnkdujai).

Interestingly, some mathematicians like Terry Tao are starting to experiment with combining LLMs with automated theorem proving, because it might help in both guiding the theorem-prover and explaining its results. I find that philosophically fascinating because LLMs rely on some practices which are not fully understood, hence the article, and may validate combining formal logic with informal intuition as a way of understanding the world (both in mathematics, and generally the way our own minds combine logical reasoning with imprecise language and feelings).

> One striking feature of mathematical culture that came up was the norm of alphabetical authorship. […] There are some exceptions, like Adleman insisting on being last in the RSA paper.

lol, took me a second to get the plausible reason for that

Its not too late to hope for the current crop of LLMs to give rise to a benevolent, patient science based educator, like the "Young Ladies Illustrated Primer" of Neal Stephensons Diamond Age.

We clearly will soon have the technology for that .. but it requires a rich opinionated benefactor, or inspired government agency to fund the development .. or perhaps it can be done as an Open model variant through crowdsourcing.

An LLM personal assistant that detects my preferences and echoes my biases and massages my ego and avoids challenging me with facts and new ideas .. whose goal is to maximize screentime and credits for shareholder value .. seem to be where things are heading.

I guess this is an argument for having open models.