math

the json file next to the problem statement in lean says the solution starts here: https://github.com/openai/math/blob/main/lean/OAI/Combinator... the proof is probably split over the constructions in the whole directory.

The approximation of edit distance result [1] seems pretty readable to me, but the learn proof is still incomplete [2]. It's certainly much less readable than a good human written proof but it's certainly better than the last generation of AI proofs. [1] https://github.com/openai/math/blob/main/preprints/An-Almost... [2] https://github.com/openai/math/blob/main/lean/ComparatorChal...

This is in the direction of Yang-Mills: https://github.com/openai/math/blob/adc7f1241b42e322a6451854...

I think a lot of the problems or gains attributed to AI are just reflections of the humans that use them. I dont care if you used AI to produce something. If you share it with me, I assume you are responsible for it. You own it, whether you agree or not. > it's causing people to be confident in information which is false, it's enabling people to treat each other like jerks in even more ways than before What is the direction of causality here? Does AI make people jerks, or they were already or prone to be jerks? The same applies to innovations or breakthroughs made by people who use AI in their work. > LLMs are solving novel math problems and successfully emulated a PS5 Did the AI independently accomplish those things, or did highly competent people accomplish them using AI as a tool? What would happen if you give someone with no mathemati

Is this not the Lean proof? https://github.com/openai/math/blob/main/lean/ComparatorChal...

https://github.com/openai/math/blob/main/preprints/An-explic... "We give a deterministic algorithm that computes the discrete Fourier transform at every length n in O ( n ( log ⁡ n ) ** (1 − 10 ** −13)) operations. The model uses exact complex arithmetic, unrestricted coefficients, specified Fourier roots, and unit-cost logarithmic-size indexing; scalar preparation and array organization are included."

It might have been updated. Is this the lean? https://github.com/openai/math/blob/main/lean/docs/180.md

Further down there is a discussion between number theorist about if the Quasi-Riemann Hypothesis is the biggest deal in 200 years or only 100. The consensus is that if a human had done it then it would deserve the Fields medal: https://news.ycombinator.com/item?id=49986803 The sub n log n result is astonishing: https://github.com/openai/math/blob/main/preprints/Integer-m... Here's a great article 2019 on the quest to achieve the n log n boundary: > Schönhage and Strassen’s ungainly n × log n × log(log n) method held on for 36 years. In 2007 Fürer beat it and the floodgates opened. Over the past decade, mathematicians have found successively faster multiplication algorithms, each of which has inched closer to n × log n, without quite reaching it. Then last month, Harvey and van der Hoeven got there. and > Harvey and van der Hoeven’s algor

Did you mean this one? https://github.com/openai/math/tree/main/preprints/The-Quasi... I thought it was interesting that it said "This paper was written with human assistance", unlike this other Quasi-Riemann Hypothesis preprint that didn't have the same disclaimer. https://github.com/openai/math/tree/main/preprints/The-Quasi...

Exactly this. If you take the entire start to finish 'agent hours' (measured comparably to man hours) they took to find all discoveries, including the go-nowhere trails that were discarded, and then divide by 90 (or whatever the exact number of results found was) it's almost certainly going to be many orders of magnitude more than 3. They provided a "snippet" of a prompt here [1] which is not only a beast, but also seems reasonably likely to have been LLM generated. So they're using LLMs to parse a vast body of mathematical work, probably including what people themselves are 'privately' working on with GPT, and then prompting other LLMs to work on such. [1] - https://github.com/openai/math/blob/main/reasoning_traces/re...

The largest I've seen [1] is an exponent of 10^12, which I suppose still counts as polynomial time. I'm sure all of these super small or large constants will improve over time, but it's still amusing. It is entertaining to see the exponents directly rather than have them hidden as n^c or epsilon or O(1). [1]: https://github.com/openai/math/blob/main/preprints/Determini...

Matrix multiplication is <=O(n^2.25) actually... [1] 1. https://github.com/openai/math/blob/main/preprints/Matrix-Mu...