Three new discoveries in mathematics, computer science, and physics
OpenAI’s claim that its models have produced proofs resolving major open problems in harmonic analysis, complexity theory, and quantum field theory — including a subexponential-time algorithm that would falsify the Exponential Time Hypothesis — is being treated as a potential watershed for AI-assisted research. Commenters explore what these results would mean for long‑standing beliefs about problem hardness, P vs NP, and the mathematical foundations of the Standard Model, while noting that the algorithms are still far from practical impact. Alongside excitement, many raise concerns about verification, credit and priority, the use of researchers’ prompts as training data, and the broader shift of high‑end theoretical work from universities into opaque private AI labs.
ETH / #SAT Breakthrough
- Thread centers on the claim “The Exponential Time Hypothesis is false” via a deterministic subexponential-time algorithm for exactly counting satisfying assignments of k-CNF (#k-SAT), with running time roughly (2^{n / (\log n)^{1/2+o(1)}}).
- This is still superpolynomial and far from polynomial; posters emphasize it does not imply P=NP or break cryptography in practice.
- There is debate over how strong the result is under common reductions: some say it undercuts many ETH/SETH-based hardness results; others note that reductions can blow up instance size so much that the subexponential bound may not transfer.
Other Mathematical and Physics Results
- Kakeya/local smoothing: resolution of Kakeya and related harmonic analysis conjectures in all dimensions is described as “Fields Medal–level” and a huge consolidation of prior piecemeal progress.
- Physics/QCD–Yang–Mills: existence of 4D Yang–Mills/QCD and a “completion” of the Standard Model is called major for rigorous quantum field theory. However, mass gap is not yet addressed, and some stress this mainly formalizes what physicists already use.
Implications for Complexity & P vs NP
- Some commenters modestly update their priors toward P=NP or undecidability of P vs NP; others see little change, pointing to the huge gap between “barely subexponential” and polynomial.
- ETH’s widespread use as a fine-grained hardness assumption means many prior results become conditional in a new way and generate many fresh open problems.
Lean Formalization and AI’s Role
- All three results have Lean formalizations; many treat the Lean theorem statements as the real ground truth.
- There is discussion that natural-language AI proofs are “raw research data” needing human distillation into understanding and theory, not just correctness certificates.
Scientific Practice, Credit, and Access
- Mixed reaction to OpenAI’s new process of recruiting “shepherd” experts and varying release strategies (immediate, Lean-only, or deferred for physics).
- Enthusiasts see this as collaborative and field-opening; critics see PR, favoritism, and private labs supplanting universities as the main site of major discoveries.
- Strong concern that models may be trained on researchers’ prompts, effectively competing with and strip-mining the very communities that feed them.
- Broader worry about centralization of scientific capability in a few private AI labs, and about math turning into “busy-work formalization” rather than human discovery.