Pinned Tweet
Linear A, the script of Bronze Age Crete, has puzzled researchers for over a century.
Today, we’re releasing the code and data behind Plasma researcher @IdaeanDaktyl’s proposed decipherment. Explore the evidence and test the readings.
plasma.ai/research/linear-a
Plasma AI retweeted
Incredibly proud of Plasma researcher @IdaeanDaktyl and his proposed decipherment of Linear A, the script of Bronze Age Crete.
Today we’re releasing the code and data behind his research so others can explore, test and build on it.
Linear A, the script of Bronze Age Crete, has puzzled researchers for over a century.
Today, we’re releasing the code and data behind Plasma researcher @IdaeanDaktyl’s proposed decipherment. Explore the evidence and test the readings.
plasma.ai/research/linear-a
Tom is continuing this research with Fractal, Plasma’s platform for coordinating teams of cloud agents around shared knowledge.
He is now applying it to other undeciphered scripts, bringing parallel investigations into a common research workspace.
We invite scholars, independent researchers and anyone curious about the ancient world to explore the material, contribute sources, and pursue their own readings.
github.com/plasma-ai/kaphtor
We then treat the random labels as vectors in a Hilbert space. Their geometry lets us partition the vertices into countably many classes. Within each class, every vertex has only finitely many neighbors in earlier layers, allowing us to assemble a proper coloring.
One final step turns this theorem into the full limit. We find disjoint finite pieces that each require many deletions per vertex, then pack copies of the same size into larger pieces. That carries the lower bound to every sufficiently large n.
The proof is public and formalized in Lean: erdosproblems.ai/111
The core theorem runs in the opposite direction: if every finite piece can be made two-colorable by deleting at most C edges per vertex, for one fixed C, then the entire graph can be colored with countably many colors.
To prove this, we build random red/blue labels through successive layers of the graph. The labels need not form a proper coloring. Instead, we control how often adjacent vertices receive matching labels.
On Monday we shared our proof of Erdős #111, posed by Erdős, Hajnal, and Szemerédi in 1979. Here’s more about what the result means and how the proof works.
Start with a graph that cannot be properly colored even with a countably infinite list of colors: 1, 2, 3, ... For each n, let h(n) be the worst-case number of edges you must delete from an n-vertex piece to make it two-colorable, as shown in the video.
We proved h(n)/n → ∞. Pick any deletion budget per vertex: a hundred, a million. For every sufficiently large n, there is an n-vertex piece that exceeds it.
Yesterday we shared our proof of Erdős #173, a geometry conjecture dating to 1973. The video shows the puzzle: color every point of the plane red or blue, and try to avoid a triangle of a chosen shape and size with all three corners the same color.
You can avoid equilateral triangles of one particular size. But then equilateral triangles of every other size must appear with all three corners the same color. So must copies of every non-equilateral triangle, with exactly the prescribed shape and size.
The surprising step in the proof: a question about triangles becomes a question about pairs. With two colors, three corners have either three matching pairs or exactly one. So knowing how often pairs match tells us how often all three corners match.
This lets us adapt @OpenAI’s recent methods, combine them with a geometric reduction from 1975, and finish with analysis.
The proof is public and formalized in Lean: erdosproblems.ai/173
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 @aturner 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