Pinned Tweet
We recently solved Erdős problems #173 and #111, two coloring problems open since 1973 and 1979. Erdős included #111 among the problems he “would most like to see solved”.
After #809 and #408, these are the third and fourth Erdős problems we’ve solved using Fractal, with all four proofs verified in Lean. We’ve also posted progress on more than 20 other Erdős problems, and we will be releasing further results in the coming weeks.
github.com/plasma-ai/erdos
Erdős #173: In 1973, Erdős, Graham, Montgomery, Rothschild, Spencer, and Straus conjectured that for any red/blue coloring of the plane, every triangle but at most one has a copy of the same shape and size with all three corners one color. We proved it, building on @OpenAI’s recent work and Lean library and the six authors’ 1975 reduction.
With two colors, a triangle that isn’t all one color has exactly one matching pair. This lets us adapt OpenAI’s method, which preserves how often pairs of points share a color, to reduce the proof to measurable colorings. We extend their key theorem to every side ratio, then finish with Bessel functions and a circle argument.
erdosproblems.ai/173
Erdős #111: In 1979, Erdős, Hajnal, and Szemerédi asked about graphs where even countably many colors (1, 2, 3, …) cannot give neighboring vertices different colors. For each n-vertex piece, find the fewest edges we must delete to make it two-colorable. Let h(n) be the largest of these numbers. We proved that h(n)/n → ∞: the number of deletions per vertex grows without bound.
Our key theorem: if h(n) ≤ Cn for a fixed C and all n, countably many colors suffice. The proof builds a random red/blue labeling layer by layer, then uses the labels as vectors to group vertices into countably many classes that are easier to color. A final argument combining disjoint finite pieces gives the limit.
erdosproblems.ai/111
More than 50 years after Erdős posed it, we have resolved Erdős problem 408: for almost all n, totient iteration takes ∼α log n steps to reach 1, for some constant α. The proof builds on @OpenAI's recent results (including their proof of the quasi-Riemann hypothesis), along with classical methods of Erdős, Granville, Pomerance, and Spiro. It is formally verified in Lean.
This is the second Erdős problem that we've fully resolved using Fractal (coming soon). We will be releasing results on more problems in the coming weeks.
erdosproblems.ai/408
Plasma AI retweeted
@nicholas_diao and I had the chance to speak with Kathryn after the OpenAI results were published. The frontier of human knowledge has never been controlled by humans. It pushes itself!
sciencenews.org/article/math…
Plasma AI retweeted
Science News featured our work at Plasma AI.
My co-founder @_andrewturner spoke about how AI is “making math more accessible.” That’s a big part of what motivates us: helping more people explore difficult problems and build on existing research.
sciencenews.org/article/math…
Erdős Problem #374 is solved! Jonathan Hartley and Matthew Olson proved the Erdős–Graham conjecture that D₆, the set of numbers needing six factorials to form a square, has positive density. They formalized the complete solution in Lean, and we verified it.
erdosproblems.ai/374
Fedir Yudin and Hartley & Olson independently completed the problem: an asymptotic for D₃ and linear growth for D₅ and D₆. Together with the known result for D₄, this settles every k from 3 to 6. Both claims are now accepted on erdosproblems.ai.
We resolved Erdős Problem 809.
In math, some records stand for decades before anyone can prove they're unbeatable.
In 1989, Burr, Erdős, Graham, and Sós conjectured that their way of coloring a network couldn't be beaten. In March 2026, Bucić, Chen, and Ma proved it for all but one case.
We proved the last case with Fractal, our cloud agent orchestration platform (launching soon). After 37 years, the conjecture is settled.
erdosproblems.ai/809
Today we’re sharing a new site tracking progress on the Erdős problems. Alongside it, we’re open-sourcing a repository which compiles results, research, and related literature. This includes our recent proof that completes Erdős Problem 809, verified in Lean.
plasma.ai/research/erdos
Our Erdős repository contains results and research pertaining to every problem, along with Markdown transcriptions from over two thousand related papers.
Recent releases of AI-generated mathematics give the results without providing insight into the process. This repository is meant to provide a format for mathematics in the world of AI. It was designed to be structured and understandable for humans and agents alike.
github.com/plasma-ai/erdos
One of the results in the repository is ours. Problem 809, posed in 1989, asks whether a simple coloring construction is optimal. Bucić, Chen, and Ma proved it for odd cycles of length 9 and up.
We proved the last case (seven-cycles) using Fractal, our cloud agent orchestration platform, launching soon. The proof is verified in Lean.
We will also be releasing results on several other Erdős problems over the coming weeks.
Our Erdős repository contains results and research pertaining to every problem, along with Markdown transcriptions from over two thousand related papers.
Recent releases of AI-generated mathematics give the results without providing insight into the process. This repository is meant to provide a format for mathematics in the world of AI. It was designed to be structured and understandable for humans and agents alike.
github.com/plasma-ai/erdos
One of the results in the repository is ours. Problem 809, posed in 1989, asks whether a simple coloring construction is optimal. Bucić, Chen, and Ma proved it for odd cycles of length 9 and up.
We proved the last case (seven-cycles) using Fractal, our cloud agent orchestration platform, launching soon. The proof is verified in Lean.
We will also be releasing results on several other Erdős problems over the coming weeks.
Our Erdős repository contains results and research pertaining to every problem, along with Markdown transcriptions from over two thousand related papers.
Recent releases of AI-generated mathematics give the results without providing insight into the process. This repository is meant to provide a format for mathematics in the world of AI. It was designed to be structured and understandable for humans and agents alike.
github.com/plasma-ai/erdos
One of the results in the repository is ours. Problem 809, posed in 1989, asks whether a simple coloring construction is optimal. Bucić, Chen, and Ma proved it for odd cycles of length 9 and up.
We proved the last case (seven-cycles) using Fractal, our cloud agent orchestration platform, launching soon. The proof is verified in Lean.
We will also be releasing results on several other Erdős problems over the coming weeks.
The prime numbers can be efficiently generated with a simple, deterministic computer program, but in many ways they "look random". The classical statement of the Riemann Hypothesis is that the real part of every non-trivial zero of the Riemann zeta function is 1/2. But it can also be stated in terms of how random the primes actually look.
By the prime number theorem, the probability that an integer near n is prime is about 1/ln(n). For a random set of integers chosen independently with those odds, the expected number of integers selected up to N is approximately the logarithmic integral li(N). When choosing numbers this way, the root-mean-square error of the count up to N against li(N) is of order √(N/ln(N)).
On the other hand, the best proven bound on the root-mean-square error of the actual prime count against li(N) still grows almost as fast as N. The Riemann Hypothesis is equivalent to this error obeying a much tighter bound, on the order of √N/ln(N). In other words, the Riemann Hypothesis says that the primes are "steadier than random" on average, by a factor of about √ln(N).