July 1944, a brick factory near Budapest, the capital of Hungary. Every time a truck loaded with freshly fired bricks reached a crossing in the rails, it bucked, and bricks spilled across the ground.

The man pushing the truck was the mathematician Pál Turán, who had been drafted into forced labor. Sweating and cursing, he found himself gripped by a single question: "what is the minimum number of crossings?"

The question became known as "Turán's brick factory problem," and for 82 years it held mathematicians at bay. On October 6, 2026 (US time), OpenAI released a set of mathematics papers written by an unreleased internal AI model, and among them it claims to have solved both this problem and its sibling, "Hill's conjecture."

How much of that claim has been checked by machine, and where does it remain only a "claim"? The clues for reading the answer lie in the history of the problem itself, which was once considered "solved" until a hole was found 11 years later.

Turán's brick factory problem Executive Summary (infographic)

Every time the rails crossed, the trucks derailed

Turán was born in Budapest in 1910. In September 1940 he was called up to a labor service unit because he was Jewish, and from then on he was moved from camp to camp.

The scene at the brick factory survives in a short piece he wrote late in life: "A Note of Welcome," the opening editorial of the Journal of Graph Theory, which was launched in 1977.

There were some kilns where the bricks were made and some open storage yards where the bricks were stored. All the kilns were connected by rail with all the storage yards. [...] the work itself was not difficult; the trouble was only at the crossings. The trucks generally jumped the rails there, and the bricks fell out of them

The lost time was precious to them, "for reasons not to be discussed here." Turán reasoned that if the number of crossings had been minimized, this loss could have been minimized too, and he asked: "But what is the minimum number of crossings?"

After several days of thought, he saw that the factory in front of him could be improved. The exact answer for the general case, with m kilns and n storage yards, looked very hard, though. He set the problem aside "to times when my fears for my family would end."

Mathematics had kept him going four years earlier, too. In 1940, at a railway construction site, an officer who heard Turán's name turned out to have worked as a proofreader at the printing shop that printed the Academy's periodical, and had seen his manuscripts. The officer reassigned Turán to a post as a guide at a wood-yard, and there, without even using paper, Turán solved a problem completely.

That problem is what is now called "Turán's theorem," the starting point of extremal graph theory. Here is how he described those days himself:

The feeling of some intellectual freedom and being, to a certain extent, spiritually free of oppression only added to this ecstasy.

Three houses, and electricity, gas and water

In its smallest form, the brick factory problem is the same as a puzzle many people tried at least once as children. Draw three lines, for electricity, gas and water, to each of three houses, without letting any lines cross.

However many times you redraw it, the last line always has to cut across another one. On a flat sheet of paper, zero crossings has been proved impossible.

A factory with three kilns and three storage yards has exactly the same shape as this puzzle. The difference is that it asks not "don't let them cross" but "make the crossings as few as possible." The answer is 1.

Three houses and their electricity, gas and water. Drawn naively, 9 crossings; placed cleverly, 1

The easiest way to picture the general case is to set the points out in two rows. Put m kilns in the top row and n storage yards in the bottom row, and connect every top point to every bottom point. That makes m×n lines in all.

You may move the points anywhere, and bend the lines as freely as you like. The brick factory problem is the search for the drawing with the fewest crossings between lines. In the language of mathematics, this figure is called the "complete bipartite graph K(m,n)," and the minimum number of crossings is called its "crossing number."

If you keep the two rows and connect them with straight lines, as on the left of the figure above, even 3×3 gives 9 crossings. Just by changing where the points sit, as on the right, the crossings drop to 1. How far you can bring them down depends on how cleverly you place things.

Split them along a cross, and the crossings fall

In 1952 Turán visited Poland and presented this problem in a talk. Two Polish mathematicians who heard it, Kazimierz Zarankiewicz and Kazimierz Urbanik, each published an answer independently.

Zarankiewicz's drawing is astonishingly simple. Draw a cross on the paper, put half the kilns to the left and half to the right along the horizontal line, put half the storage yards above and half below along the vertical line, and connect everything with straight lines.

Zarankiewicz's drawing: 4 kilns and 7 storage yards give 18 crossings

The number of crossings this drawing produces can be calculated with the formula below. ⌊ ⌋ is the symbol for "round down, dropping everything after the decimal point."

Z(m, n) = ⌊m/2⌋ × ⌊(m−1)/2⌋ × ⌊n/2⌋ × ⌊(n−1)/2⌋

The calculation is easier than it looks. Halve the number on one side and round down; subtract 1 first, halve and round down; multiply the two. Do this for both sides, then multiply the results together.

  • 3×3 (the three houses): (1×1)×(1×1)＝1
  • 2×n: The side with 2 points gives (1×0)＝0, so it can be drawn with zero crossings however many points the other side has
  • 4×7 (the figure above): (2×1)×(3×3)＝18
  • 10×10: (5×4)×(5×4)＝400

In 1954 Zarankiewicz published a paper with a proof that this drawing is the best possible, that no drawing whatsoever can have fewer crossings. At this point, the problem was "solved" for the first time.

"It can be drawn" and "you can't do better" are different jobs

This is where the real difficulty of the problem shows itself. To show that "it can be drawn with 18 crossings," it is enough to actually draw one.

To show that "it can never be drawn with 17 or fewer," on the other hand, you have to rule out every imaginable drawing, without exception. The points can sit in infinitely many places, and the lines can twist and wind however they like.

In mathematics the first is called an "upper bound" and the second a "lower bound." An upper bound needs only one concrete example, but a lower bound is a blanket denial: "no matter how clever you are, it cannot be done."

An upper bound can be shown by drawing one picture, but a lower bound has to take on every drawing

OpenAI's paper itself states this plainly: "Counting crossings in prescribed drawings gives upper bounds; establishing the minimum over all drawings also requires a lower-bound argument."

A hole in the proof that no one noticed for 11 years

Zarankiewicz's proof appeared in the prestigious journal Fundamenta Mathematicae and was treated as a theorem for more than ten years. The hole was found by Paul Kainen in 1965 and Gerhard Ringel in 1966. Each of them noticed, independently, that part of the induction did not hold.

The proof took the form of an induction, building up the conclusion as the number of points grew. The step from an odd number of points to an even one was correct, but the step from even to odd did not hold.

In 1969 the British-born mathematician Richard Guy wrote up the whole affair in a paper titled "The decline and fall of Zarankiewicz's theorem." The "theorem" was demoted to a "conjecture."

Zarankiewicz himself had died in 1959, before the hole was found. He too carried scars from the war: under German occupation he had taken part in forbidden underground teaching and had been sent to a concentration camp.

In his 1977 note of welcome, Turán wrote:

But Ringel found a gap in his published proof, which nobody has been able to fill so far—in spite of much effort.

A map filled in, bit by bit

The half century after the hole was found was a history of slowly widening the range confirmed to be correct.

  • 1970: Daniel Kleitman proved the formula correct when one side has 6 points or fewer
  • 1993: Douglas Woodall confirmed cases such as 7 columns × 7 to 10 by computer
  • 2006: de Klerk and colleagues proved that, even in large cases, at least 83% of the formula's value in crossings is unavoidable
  • 2023: Balogh and colleagues raised this share to about 91% for the case where both sides have the same number of points

Kleitman also showed that if there is any case where the formula is wrong, then in the smallest such case both sides must have an odd number of points. Even so, a proof covering every case remained out of reach.

This problem has a sibling. Instead of splitting the points into two rows, connect every pair of n points with a line: the crossing number of the "complete graph." The first people to find the conjectured formula for this one were not mathematicians but the British constructionist painter Anthony Hill and his friend, the American painter John Ernest.

The formula the two had arrived at by the spring of 1959 was introduced by Guy in a 1960 paper, and in 1963 Hill himself published it with the mathematician Frank Harary as coauthor. This is the "Harary–Hill conjecture (Hill's conjecture)." For 5 to 14 points, the crossing numbers the formula predicts run 1, 3, 9, 18, 36, 60, 100, 150, 225, 315.

A drawing that follows Hill's formula: 8 points set in a straight line, with the lines split above and below, give 18 crossings

Here too, the formula had been confirmed only up to 12 points (Pan and Richter, 2007) and for 13 and 14 points (Aichholzer, 2021). Both were proofs that relied on computers. Guy died in March 2020 at 103, and Hill in October of the same year at 90.

Timeline from 1940 to 2026

What does OpenAI claim to have "solved"?

What OpenAI released is a GitHub repository, "openai/math." It bundles 722 papers into 372 "result families," and according to the README the model was posed approximately 4,000 open problems, with each result using, on average, roughly three hours of ChatGPT Pro thinking compute.

The brick factory problem appears as entry 165. Its heading is "The Harary–Hill and Zarankiewicz crossing-number formulas," and its description reads:

Resolves the Harary–Hill conjecture and Turán's brickyard problem in the Zarankiewicz formulation, determining the crossing numbers of every complete and complete bipartite graph.

The scope of the claim is, quite literally, "everything."

  • The brick factory problem (Zarankiewicz's conjecture): For all positive integers m and n, the crossing number equals Z(m, n)
  • Hill's conjecture: For every number of points n, the crossing number of the complete graph equals Hill's formula

What had been confirmed before 2026, and what is now claimed

Behind this stand two papers, both with "OpenAI" as author and both dated September 23, 2026. The complete-graph paper is 13 pages and the bipartite paper 16 pages, short as proofs of a half-century-old problem go.

For Hill's conjecture, what had been shown for every n until now were cases with restrictions on the drawing, such as "only if the points are set on a straight line and the lines are split above and below it." The new paper places no such restriction, and instead converts the drawing itself into algebraic information.

Concretely, it records in tables of numbers (matrices) which way each pair of lines crosses and in what order the lines leave each point, and carries this into inequalities of linear algebra. In the paper's own words, "The proof separates the geometry of a drawing from two linear-algebraic statements."

What Lean has checked, and what has not been checked yet

What sets this claim apart from the familiar "AI solved a hard problem" story is that it comes with a formal proof in Lean. Lean is a programming language for having a computer check a mathematical proof line by line.

On Lean, the shortcut "this part is obvious" and trust in a prestigious journal are both powerless before the check. If there were a hole in the induction, like the one in Zarankiewicz's proof, the check would stop right there.

According to the repository's description (lean/docs/165.md), the scope of the Lean formalization is as follows.

  • Hill's conjecture: Proves that the crossing number equals Hill's formula for every number of points n of 3 or more. Besides proving the lower bound, it actually constructs a drawing with exactly the formula's number of crossings
  • Zarankiewicz's conjecture: Proves the equality for all positive integers m and n, and constructs a drawing that attains the formula's value

The formalized definition of "crossing number" can also be checked in the challenge files. The points are placed at distinct positions in the plane, and a line may be as twisted as you like, as long as it is a continuous curve that does not cross itself.

Crossings are finite in number; drawings with points where lines merely touch, or where three lines meet at a single point, are excluded; and if the same two lines cross several times, each crossing counts once. These are the conventions long used as standard in research on crossing numbers.

The published files run to 339 files and about 20,600 lines on the bipartite side, and 46 files and about 18,000 lines on the complete-graph side. As far as a search of both folders showed, the count of "sorry" for skipping a proof, and of added custom axioms, was zero.

On the other hand, it is also clear what a Lean check does not guarantee.

  • Whether the statement is written correctly: What Lean confirms stops at the fit between the "formalized statement" and the "formalized proof." Whether that statement really is the same as the conjecture mathematicians mean is for a human reader to judge
  • Re-verification by a third party: As of October 7, 2026, reports of an outside researcher running this check in their own environment stood at zero, as far as could be found
  • Peer review of the papers: The 13-page and 16-page papers themselves are still at the pre-peer-review stage
  • Novelty and credit: Whether the ideas are truly new, or a combination of existing research, lies outside what Lean covers

How far has it been verified? (as of October 7, 2026)

Andrew Sutherland, a mathematician at the Massachusetts Institute of Technology, told Scientific American about the release as a whole: "Until and unless they release the model and people can replicate their results, I think you should treat any claims about one-shotting problems with a single agent as unverified. We should ask for receipts." As of October 7, expert commentary specifically on entry 165 stood at zero, as far as could be found.

There is also a precedent that shows the distance between a claim and a proof. In 2018, two researchers published a paper in an engineering journal claiming to have shown the formulas of both conjectures. OpenAI's paper mentions it and points out that counting a prescribed drawing alone does not give a lower bound.

The 11-year hole, and a machine's check of the arithmetic

Zarankiewicz's proof survived for 11 years because the people who read it trusted a prestigious journal and the name of a distinguished mathematician. Human peer review sometimes lets holes slip through on trust.

Lean believes only the result of its line-by-line check. Ironically, this proof written by an AI arrives in a form ready, from the outset, for a kind of check that the proof a human wrote 70 years ago never once received.

The shape of the question changes, though. As machines take on much of "is the proof correct?", questions like "did it prove the right question in the first place?" and "is there a new idea in the proof?" remain on the human side.

This pattern applies just as well outside mathematics. When you receive a report or code written by AI, you need to read it in at least 3 separate layers.

  • The claim: what the AI says it "did"
  • The machine-verified range: the parts where tests or formal verification actually passed
  • The range people must judge: whether the question was framed correctly, and whether it is truly useful

The difference between an "upper bound" and a "lower bound" is also a yardstick you can carry straight into a meeting room. "This measure cut costs by 20%" can be said by showing a single success. "There is no way to cut any further" is a far heavier claim, one you should only make after knocking down every alternative.

A reply that arrived 82 years later

Turán closed his "Note of Welcome" like this:

So I close it by expressing my wish and hope that I shall be able to read among many other important results the solution of the abovementioned open problems as well in this periodical.

The piece appeared in the journal only after his death. He had died of leukemia on September 26, 1976, at the age of 66. His wife, the mathematician Vera Sós, kept the diagnosis from him, and his close friend and collaborator Paul Erdős later lamented that Turán had died with work he had put off "for later."

Eighty-two years after the trucks jumped the rails, the reply arrived, written by a machine, in a GitHub repository rather than the specialist journal Turán had hoped for. Whether it is the answer Turán was waiting for will be decided by the human mathematicians who read the results of the Lean check and work through the papers.

References