A Proof Checker Is Not a Building Permit

Today OpenAI claimed it solved a 100 year old math problem with AI.

The problem is called Navier-Stokes. It asks how fluids like water and air move, and whether the math that describes them can ever break down. It is one of seven Millennium Prize Problems, with a one million dollar prize for a correct solution.

OpenAI says its AI system produced a full proof, plus a computer check in a language called Lean that verifies each logical step. OpenAI says it used on the order of 10,000 AI agents working in parallel for about 88 hours, followed by about 17 hours to complete the Lean check.

That part is impressive. But it is not the most useful part for construction.

What OpenAI actually claimed

Here is the careful context, in plain words. OpenAI claims a very specific result. It built a special, smooth pushing force that starts a fluid from rest and makes the speed grow without limit in a finite time, while total energy stays bounded. It says this matches two allowed paths in the official Clay prize statement, known as C and D, which do allow a smooth force.

It does not claim the same breakdown happens with no force at all. And as of September 9, 2026, Clay still lists Navier-Stokes as Unsolved. A computer check is strong evidence, but it still needs independent review by mathematicians and a formal decision by Clay, which takes years. There is also an open dispute about credit, because other researchers had been working on a related approach.

So no, fluids are not broken. Your flow software still works. No bridge design changes tomorrow.

The real question for us is different.

Why this matters for construction

A lot of construction engineering work is solving complex problems under pressure. How to size a temporary bridge. How to sequence 500 activities with limited cranes and crews. How to place loads during construction without overstress. These problems usually rely on a few experienced people, spreadsheets, rules of thumb, and long review cycles.

Can AI solve this type of problem accurately and fast, and in a way we can trust and audit? That is what we wanted to test.

The lesson from OpenAI is not speed. It is not the 10,000 agents. It is this: let AI agents propose many ideas, but let a small, open checker decide what passes, and keep every step visible.

We built a simple demo to show how that works in construction.

The problem we picked, and why it is hard

We picked a 20 meter temporary steel access truss bridge. Think of a small construction bridge used to carry equipment and workers over a gap for a few months.

It sounds simple. It is not.

You have to choose the layout pattern: Pratt, Howe, Alternating, or X bracing. You have to choose steel sizes for four groups: bottom chord, top chord, verticals, and diagonals. We allowed 16 tube sizes, from small 60 mm tubes to large 355 mm tubes. That alone gives more than 250,000 possible combinations, before you even consider layout.

Then you have to check each idea against real physics:

• Three different load cases. Full construction load across the whole bridge. Heavy load on only one side, which often controls. Plus wind pushing with gravity.
• Weight of the steel itself, which changes every time you change a size.
• Pulling apart. Each member in tension must stay below its safe limit.
• Buckling. Long thin members in compression can buckle long before the steel yields. Short members behave differently from long ones.
• Sag. The bridge cannot deflect more than span divided by 500, which is 40 mm for a 20 meter span.
• Stability. The whole frame must be stable, not a mechanism, and forces must balance at every joint.

A human engineer would normally pick two or three trial designs based on experience, run them through analysis software, adjust sizes up where it fails, and repeat. For a careful study with several patterns and load cases, that is easily days of work, and you still only check a tiny slice of the options. You never know if a lighter safe design was missed.

Our agents checked 2,860 full designs in minutes on a normal laptop, using only open Python code. No black box. Every design went through the same physics solver.

How our agents solved it

We used a simple team, with a strict rule.

Generators proposed designs. They could only pick from the allowed list of patterns and tube sizes. They could not change the rules.

A single open solver did all the checking. It is a standard 2D truss stiffness model in Python. It builds the structure, applies supports and loads, solves for movement at each joint, recovers the force in each member, and checks tension, buckling, and deflection. About 200 lines of clear code. Anyone can read it and rerun it.

The search ran in two phases. First, start big and safe, then step each group down until it almost fails. Second, try random small changes to sizes and patterns, and keep only changes that lower weight while still passing all checks. The seed is fixed, so the run is repeatable.

This separation matters. Agents are creative but can make mistakes. The solver is dumb but honest. Only the solver can say pass or fail. That is the same idea as OpenAI's Lean check, just applied to steel instead of fluids. Generate fast, verify with a visible tool.

What it found

Start point: an oversized all heavy tube design at 10,525 kg of steel.

End point: an Alternating pattern at 1,938 kg. That is an 81.6 percent saving, while still passing every check.

The winning sizes are easy to state:

• Bottom chord: 168.3 mm by 6.3 mm tube
• Top chord: 168.3 mm by 8.0 mm tube
• Verticals: 60.3 mm by 3.6 mm tube
• Diagonals: 139.7 mm by 6.3 mm tube

Results:

• Uniform full load: sag 38.1 mm, peak use 91 percent of capacity
• One sided heavy load: sag 35.8 mm, peak use 86 percent
• Wind plus gravity: movement 17.2 mm, peak use 44 percent

Supports: about 310 kN on each side under full load. About 331 kN left and 216 kN right under one sided load. Wind case adds about 80 kN horizontal push.

Independent checks: force balance error less than 0.000000003 N. Stiffness matrix full rank. Residuals near zero. In plain words, the math balances.

You can see the full figures and animation in our LinkedIn post: the final shape colored by stress, the three bent shapes under the three loads, the bar chart showing all 41 members below 100 percent, and the learning curve dropping fast then flattening.

This is powerful because it did not just find one answer. It showed the whole trade. It kept a log of all 2,860 tries, with 71 step improvements along the way. You can audit why the winner won.

What this means for scheduling, structural work, and field decisions

The same pattern fits many construction problems.

For structural temp works: scaffolds, formwork, shoring towers, crane mats, excavation bracing. The physics changes, but the loop is the same. Define the spec, let agents propose layouts and sizes, let an open checker enforce limits, keep the log.

For scheduling: activities, logic, crew limits, crane limits, delivery windows. Let agents propose sequences, let a scheduler check dates, floats, and resource overloads, keep the log. You get options in hours instead of weeks, with reasons you can show an owner.

For cost and carbon: same candidates, transparent unit rates and factors. No hidden score. Mass, cost, and carbon reported separately.

The key is auditability. If a third party cannot rerun the same candidate and get the same result, it is persuasion, not verification. If agents can quietly change the checker, it is not safe. If provenance is missing, you cannot defend the decision.

What we are not claiming

This demo is conceptual and educational only. It is not for construction. It is not safe, approved, code compliant, or buildable.

A real temporary bridge needs much more: governing code combinations, 3D stability and bracing, connections and welds and bolts, deck behavior, dynamics and impact, fatigue, wind out of plane, foundations and scour, erection sequence, tolerances, corrosion, inspection, permits, and a licensed engineer in charge. Our 2D model leaves all of that out on purpose, to keep the lesson clear.

Just like a Lean check is not a Clay prize, a Python pass is not a building permit. Slow review by qualified people and authorities is part of verification, not red tape.

Try it yourself

All files are open: solver.py runs the whole study, results.json holds the winner and all load cases, convergence.csv holds all 2,860 evaluations, and technical_report.md states assumptions and limits. Run python3 solver.py. You should get the same 1,938 kg Alternating design, same 38.1 mm sag, same 0.91 peak use.

If AI can help prove math and can help search steel, the future for construction is not AI replacing engineers. It is engineers who use auditable AI to explore far more options, with clearer proof of what passed and what did not.

That is a future worth building.

Sources accessed Sep 9, 2026: OpenAI announcement, OpenAI Lean repo, Clay formulation (Fefferman PDF), Clay status: Unsolved, Quanta Magazine, Buckmaster statement (PDF)

Disclaimer: Conceptual demonstration only. Not permit ready design. Do not use for fabrication, erection, or public use. Requires licensed engineer review and authority approval for any real project.