More

I am a Math Engineer at Math, Inc., and will soon join the AI for Science team at OpenAI.

Hi there! I am a 21-year-old British pure mathematics undergraduate university student at the University of Cambridge at Queens' College, interested in sieve theory and analytic number theory more generally. I am especially fascinated by $L$-functions and their special values. I have also become engrossed by automated theorem proving and future uses of artificial intelligence in this area.

I like evaluating integrals and series as a pastime as you can see on my MSE below:

My MSE/MO can be found here: https://math.stackexchange.com/users/885224/kstar
My blog can be found here: https://kb799.user.srcf.net/

I and Liam have now obtained the first confirmed solution to a FrontierMath open problem (see this X thread should you be interested). We had taken a break from Erdős problems for the past two months or so (although I had a rare free day from university work to just try [457] which previously seemed rather easy to me, and got it via GPT immediately, so I suspect there are lots of remaining low-hanging fruit problems) just out of burnout.

I’m now on my Easter break from university, so I intend to now return to trying to get more solutions here out of interest.

> The [Er79d] formulation is simply the negation of the [ErGr80] formulation.
Ah yes! I skim-read a little too fast. I think the better option is to absorb the more non-trivial general question into the problem statement, perhaps.

GPT-5.2 Pro gives an extremely elementary argument for any $0<\epsilon<\frac{3}{\log 4}-2$ viewable as a PDF here. This is certainly a very easy problem as stated, so I am suspicious ([ErGr80] seems to state it this way as well). Going into [Er79d] seems to ask about the opposite direction inequality for sufficiently large $n$:
"Is it true that $q(n,[\log n])<(2+\varepsilon)\log n$ for $n>n_0(\varepsilon)$?"

I suspect this is the actual intended direction? Anyhow, Aristotle did autoformalise its solution to the problem as stated on the site here. ChatGPT Deep Research failed to find anything substantive in the literature (sharing its chat link results in an error, but one can view its generated PDF report here). GPT-5.2 Pro failed at constructing an argument for the more general problem in the description.

Update: In an independent, again autonomous run, GPT-5.2 Pro has given an alternative argument utilising PNT that resolves the stated question for arbitrarily large $\epsilon$: See here.

I've personally moved on to other things. Haven't tried throwing Erdős problems at the models for a while. Maybe I'll go back to it when GPT-5.3 Pro releases.

FYI, we know there are loads of bugs that can even pass SafeVerify. James Hanson in the Lean Zulip has been cataloguing such things well, e.g. here is a truly marvelous proof of FLT that can fit in one's margins, only depends on propext, and passes both SafeVerify & lean4checker!

Looking past the romanticisation of Lean, if one knows what they are doing and they are not doing things in good faith, it is very easy to find exploits. It is not as robust as one may hope. One should be very wary that a future hypothetical mathematical superintelligence will likely be able to find and exploit such bugs at scale, and it would be infeasible for humans to check it all.