Background

On October 26th, openAI announced AI generated solutions to three open math problems in harmonic analysis, mathematical physical, and complexity theory.

The complexity theory paper The Exponential Time Hypothesis is False, gives a $2^{o(n)}$ time algorithm for solving (and indeed counting solutions to) a k-CNF formula, thus disproving the Exponential Time Hypothesis of Impagliazzo, Paturi, and Zane.

More specifically, they released a repository which contained a paper with a natural language proof of a

$(n+m)^{O_k(1)} \cdot 2^{O_k(n \log\log n / \sqrt{\log n})}$

algorithm, and a Lean formalization of a slightly weaker bound.

Anthropic also subsequently released a different proof and Lean formalization (also AI generated) of a similar result.

This site is aimed at facilitating discussion around these results within the math and computer science community.