Tag: math

Competitive AI

OpenAI:

We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems. These problems are not standard math exercises, they are used to let the best high-school students compete against each other. The prover uses a language model to find proofs of formal statements. Each time we find a new proof, we use it as new training data, which improves the neural network and enables it to iteratively find solutions to harder and harder statements. We achieved a new state-of-the-art (41.2%) on the miniF2F benchmark, a challenging collection of high-school olympiad problems.

DeepMind:

we created a system called AlphaCode that writes computer programs at a competitive level. AlphaCode achieved an estimated rank within the top 54% of participants in programming competitions by solving new problems that require a combination of critical thinking, logic, algorithms, coding, and natural language understanding.

Wavelets

Built upon the ubiquitous Fourier transform, the mathematical tools known as wavelets allow unprecedented analysis and understanding of continuous signals.

Fourier transforms have a major limitation: They only supply information about the frequencies present in a signal, saying nothing about their timing or quantity. It’s as if you had a process for determining what kinds of bills are in a pile of cash, but not how many of each there actually were. “Wavelets definitely solved this problem, and this is why they are so interesting” A signal could thus be cut up into smaller areas, each centered around a specific wavelength and analyzed by being paired with the matching wavelet. Now faced with a pile of cash, to return to the earlier example, we’d know how many of each kind of bill it contained. Part of what makes wavelets so useful is their versatility, which allow them to decode almost any kind of data. “There are many kinds of wavelets, and you can squish them, stretch them, you can adapt them to the actual image you are looking at”. The wave patterns in digitized images can differ in many aspects, but wavelets can always be stretched or compressed to match sections of the signal with lower or higher frequencies. The shapes of wave patterns can also change drastically, but mathematicians have developed different types, or “families,” of wavelets with different wavelength scales and shapes to match this variability.

Hypergraphs

The higher-order analogue of a graph is called a hypergraph, and instead of edges, it has “hyperedges.” Purvine and her colleagues analyzed a database of biological responses to viral infections, using hypergraphs to identify the most critical genes involved. They also showed how those interactions would have been missed by the usual pairwise analysis afforded by graph theory. However, generalizing from graphs to hypergraphs quickly gets complicated. There are lots of ways of generalizing this notion of a cut to a hypergraph. But there’s no one clear solution, because a hyperedge could be severed various ways, creating new groups of nodes.

2023-04-13: Another powerful concept only very vaguely related are Hypervectors (though this Github project seems to allow you to play with both)

Hyperdimensional computing promises a new world in which computing is efficient and robust, and machine-made decisions are entirely transparent.
Hyperdimensional computing tolerates errors better, because even if a hypervector suffers significant numbers of random bit flips, it is still close to the original vector. Another advantage of hyperdimensional computing is transparency: The algebra clearly tells you why the system chose the answer it did. The same is not true for traditional neural networks. It’s also compatible with “in-memory computing systems,” which perform the computing on the same hardware that stores data (unlike existing von Neumann computers that inefficiently shuttle data between memory and the central processing unit). Some of these new devices can be analog, operating at very low voltages, making them energy-efficient but also prone to random noise. For von Neumann computing, this randomness is “the wall that you can’t go beyond”. But with hyperdimensional computing, “you can just punch through it.”

Turing Patterns

Turing’s paper described a theoretical mechanism based on 2 substances — an activator and an inhibitor that diffuse across an area at different rates. The interaction between these 2 “morphogens,” as Turing called them, allows one to interrupt the effect of the other — creating a pattern of colored lines on a tropical fish, for example, rather than a solid color. Turing’s mechanism was indeed responsible for the stripes in the bismuth. And it demonstrated once again how robust and powerful Turing’s original insight was. Here, the stripe-forming process is driven by the forces at play among the bismuth atoms and the metal below. Bismuth atoms want to fit into particular spots on the molecular lattice of the metal. But these spots are closer together than the bismuth atoms find comfortable. Like a photograph that gets shoved into a frame that’s too small for it, the sheet of bismuth atoms buckles. The strain creates a wavy pattern that leaves some atoms raised, forming the stripes. The vertical shift — movement away from the plane of the crystal — acts as the activator in the Turing equations, while the shift within the plane acts as the inhibitor. The morphogens here are displacements, not molecules. When part of a Turing pattern is wiped out, it grows back. You might not assume that inorganic materials like bismuth crystals would be able to heal as animals do,but indeed, his team’s simulated bismuth crystal was able to mend itself.

Animal Numerosity

Practically every animal that scientists have studied — insects and cephalopods, amphibians and reptiles, birds and mammals — can distinguish between different numbers of objects in a set or sounds in a sequence. They don’t just have a sense of “greater than” or “less than,” but an approximate sense of quantity: that 2 is distinct from 3, that 15 is distinct from 20. This mental representation of set size, called numerosity, seems to be “a general ability,” and an ancient one. Many species have displayed a capacity for abstraction that extends to performing simple arithmetic, while a select few have even demonstrated a grasp of the quantitative concept of 0 — an idea so paradoxical that very young children sometimes struggle with it. Both monkeys and honeybees know how to treat 0 as a numerosity, placing it on a mental number line much as they would numerosity 1 or 2. And crows can do it, too.

First Applied Geometry

Researchers have made a discovery that may shake up the history of mathematics, revealing evidence of applied geometry being used for the purposes of land surveying 3.7 ka BP. Found on a Babylonian clay table, the etchings are believed to represent the oldest known example of applied geometry, and feature mathematical techniques linked to the Greek philosopher Pythagoras that were well ahead of their time.

0.001% Mathlib

When Lean came out, there were plenty of other proof assistants available, including Coq, which is the most similar to Lean — the logical foundations of both programs are based on dependent type theory. But Lean represented a chance to start fresh. Mathematicians created mathlib and eagerly began to fill it with the world’s mathematical knowledge. The work has the air of a barn raising. “If you were to quantify how much of mathematics is formalized, I’d say it’s way less than 0.001%.” It will probably take decades before mathlib has the content of an actual research library, but Lean users have shown that such a comprehensive catalog is at least possible — that getting there is merely a matter of programming in all the math. Last year, the Lean community put aside the accumulation of undergraduate math and skipped ahead to the vanguard of the field. The goal was to define one of the great innovations of 21st-century mathematics — an object called a perfectoid space that was developed over the last 10 years by Peter Scholze. In 2018, the work earned Scholze the Fields Medal.

This project just hit a major milestone, as Peter Scholze explains:

While this challenge has not been completed yet, I am excited to announce that the Experiment has verified the entire part of the argument that I was unsure about. I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research. Congratulations to everyone involved in the formalization!!

In this Q&A-style blog post, I want to reflect on my experience watching this experiment.

How did the formalization proceed?
Initially, I imagined that the first step would be that a group of people study the whole proof in detail and write up a heavily digested version, broken up into many many small lemmas, and only afterwards start the formalization of each individual lemma. This is not what happened. Instead, the formalization followed quite closely the original lecture notes, and directly attacked Lemma after Lemma there. It did seem that the process was to directly type the proofs into Lean. Lean actually gives the user a very clear summary of what the current goal is, so one always needs to get a very clear sense of what the next few steps really are. Sometimes it was then realized that even on paper it does not seem clear how to proceed, and the issue was brought to attention in the chat, where it was usually quickly resolved. Only after a lemma was entirely formalized, the proof, now thoroughly digested, was again written up in the Blueprint in human readable form.

What did you learn about the process of formalization?
I learnt that it can now be possible to take a research paper and just start to explain lemma after lemma to a proof assistant, until you’ve formalized it all! I think this is a landmark achievement.

see also this earlier piece about using coq:

For 10 years, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people. “The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes”. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. The real potential of type theory informed by homotopy theory is as a new foundation for mathematics that’s uniquely well-suited both to computerized verification and to studying higher-order relationships.

and even earlier efforts:

A grand objective of the field is to formalize the whole of mathematics, reproving its theorems with a negligible probability of error, all based on a small kernel (in the HOL Light system, the kernel is 500 lines of OCaml code).

and another backgrounder

As the towering mathematical enterprise reaches new heights, with more intricately and esoterically turreted peaks, each practitioner drilling down into minutiae that could never be understood by colleagues even in the same field, computers will be necessary for advancing the enterprise, and authenticating the integrity of the structure—a structure so complex in detail and so massive in scale that adjudication by mere human referee will no longer be feasible

one person’s perspective

I’m not concerned by the fact that no human mathematician can check this, because we can check it with other computer approaches

2023-06-01: Progress continues, and now LLM have entered the picture

We set out to tackle serious mathematics with a combination of hope and trepidation. We were able to formalize everything we set out to formalize and were never forced to discard a development part way through. “We have formalized results by 2 Fields medalists (Roth and Gowers), an Abel prize winner (Szemerédi) and of course Erdős too!” We’ve also seen impressive advances in search and language models to assist users in proof development. Although the effort required to formalize mathematical articles remains high, we can confidently predict that formalization will be playing a significant role in mathematical research in the next few years.

2025-09-11: Gauss

Using Gauss we produced ~25K lines of Lean code, comprising 1K theorems and definitions. Formal proofs of this scale have historically been major milestones, often the culmination of multi-year efforts. The largest singular formalization projects in history — career-defining efforts, which can span more than a decade — are only an order of magnitude larger at up to 500K LOC. Lean’s standard mathematical library, Mathlib, is 1 OOM beyond that, at 2M LOC, comprising 350K Lean theorems and definitions, and developed by 600 human contributors over 8 years. With further algorithmic improvements, we aim to increase the sum total of formal code by 2-3 OOM in the coming 12 months. This will serve as the training ground for a new paradigm — verified superintelligence and the machine polymaths that will power it.

Fractals Everywhere

The genes that cause Romanesco, a kind of cauliflower, to grow in a fractal pattern have been identified. “we found that curd self-similarity arises because the meristems fail to form flowers but keep the ‘memory’ of their transient passage in a floral state. Additional mutations affecting meristem growth can induce the production of conical structures reminiscent of the conspicuous fractal Romanesco shape. This study reveals how fractal-like forms may emerge from the combination of key, defined perturbations of floral developmental programs and growth dynamics.”

It’s the fact that this gene appears to function in other plants, though, that is blowing my mind. Give this technique another 10 or 20 years, and the resulting experiments—and the subsequent landscapes—seem endless, from gardens of infinitely self-similar roses and orchids to forests populated by bubbling forms of fractal pines, roiling oaks, and ivies.

Numbers inevitable?

Why do we use numbers so much? Is it something about the world? Or is it more something about us? We discussed above the example of fundamental physics. And we argued that even though at the most fundamental level numbers really aren’t involved, our sampling of what happens in the universe leads us to a description that does involve numbers. And in this case, the origin of the way we sample the universe has deep roots in the nature of our consciousness, and our fundamental way of experiencing the universe, with our particular sensory apparatus, place in the universe, etc. As long as we preserve core aspects of our experience as what we consider conscious observers some version of numbers will in the end be inevitable for us. We can aspire to generalize from numbers, and, for example, sample other representations of computational reducibility. But for now, numbers seem to be inextricably connected to core aspects of our existence.