08-20-2026, 08:54 PM
What Happens When the World Is Run on Code No One Understands?
Authors: Patrick Shafto, Ken Ono, Scott Duke Kominers
Published: August 20, 2026 — TIME
The article argues that AI is creating a fundamental shift in science and software engineering: generating discoveries, proofs, and code is becoming easier than verifying them. The authors point to recent cases in mathematics where AI systems produced results that required teams of expert mathematicians to translate and validate. Their central claim is that the traditional bottleneck—human discovery—is being replaced by a new bottleneck: human verification. As AI produces enormous quantities of sophisticated output, society increasingly faces the possibility of relying on mathematical proofs, software, and technical systems that work but that few—or perhaps no—humans fully understand.
This problem becomes especially dangerous when AI-generated code enters critical infrastructure such as hospitals, banking systems, transportation, defense systems, and power grids. Generative AI and “vibe coding” allow software to be produced much faster, but the resulting systems may contain subtle vulnerabilities or behave in unexpected ways. The authors therefore advocate formal verification: mathematically specifying what a program is supposed to do and producing machine-checkable proofs that the program satisfies those specifications. Instead of trusting code because programmers inspected it, we could increasingly trust it because a formal proof checker has verified its logical correctness.
However, formal verification does not eliminate the human role. Once checking proofs becomes cheap, the critical challenge becomes writing the correct specification. A perfectly verified program can still be disastrous if humans specified the wrong objective or failed to model an important real-world condition. The authors therefore propose major investment in mathematical research, verified software libraries, common specifications, standards, benchmarks, education, and collaboration between mathematics, computer science, engineering, and national security. Their broader message is striking: AI may make mathematics more important, not less, because mathematical rigor could become the foundation that allows society to trust increasingly autonomous software systems.
Key takeaways
Old world:
AI world:
That shift—from human-readable code to machine-verifiable correctness—is essentially the article's central thesis.
ARTICLE
Authors: Patrick Shafto, Ken Ono, Scott Duke Kominers
Published: August 20, 2026 — TIME
The article argues that AI is creating a fundamental shift in science and software engineering: generating discoveries, proofs, and code is becoming easier than verifying them. The authors point to recent cases in mathematics where AI systems produced results that required teams of expert mathematicians to translate and validate. Their central claim is that the traditional bottleneck—human discovery—is being replaced by a new bottleneck: human verification. As AI produces enormous quantities of sophisticated output, society increasingly faces the possibility of relying on mathematical proofs, software, and technical systems that work but that few—or perhaps no—humans fully understand.
This problem becomes especially dangerous when AI-generated code enters critical infrastructure such as hospitals, banking systems, transportation, defense systems, and power grids. Generative AI and “vibe coding” allow software to be produced much faster, but the resulting systems may contain subtle vulnerabilities or behave in unexpected ways. The authors therefore advocate formal verification: mathematically specifying what a program is supposed to do and producing machine-checkable proofs that the program satisfies those specifications. Instead of trusting code because programmers inspected it, we could increasingly trust it because a formal proof checker has verified its logical correctness.
However, formal verification does not eliminate the human role. Once checking proofs becomes cheap, the critical challenge becomes writing the correct specification. A perfectly verified program can still be disastrous if humans specified the wrong objective or failed to model an important real-world condition. The authors therefore propose major investment in mathematical research, verified software libraries, common specifications, standards, benchmarks, education, and collaboration between mathematics, computer science, engineering, and national security. Their broader message is striking: AI may make mathematics more important, not less, because mathematical rigor could become the foundation that allows society to trust increasingly autonomous software systems.
Key takeaways
- AI-generated output may soon exceed humanity's ability to inspect it manually.
- The new scarce resource is increasingly verification rather than discovery.
- Formal methods and machine-checkable proofs could provide a scalable way of validating AI-generated software.
- Verification alone is insufficient: humans must still decide what the system should actually do.
- Mathematics could become a core part of AI safety and software infrastructure, providing a transition from “trust the programmer” to “verify the proof.”
Old world:
Code:
Human writes code → humans inspect it → software is trustedCode:
AI writes code → mathematical specification → automated proof/verification → software is trustedThat shift—from human-readable code to machine-verifiable correctness—is essentially the article's central thesis.
ARTICLE
┌────────────────────────────────┐
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘