pull down to refresh

The proof I submitted for Erdos Problem #397 was accepted by Terence Tao. The proof was generated by GPT 5.2 Pro and formalized with Harmonic. Many open problems are sitting there, waiting for someone to prompt ChatGPT to solve them.

The other two problems were #728 and #729

Terence Taos comment about 728:

reply
5 sats \ 1 reply \ @gmd 2h

we’ve reached super intelligence. Only a minuscule percent of humans can even understand the math problems AI is tackling.

reply

Using AI and prompting it correctly is still harder than most people think. Especially if you've ever created something that was supposed to use agentic tools (e.g. via LangChain).

reply
Erdos Problem #397 was accepted by Terence Tao

There is something beautiful in Terence being the one accepting the solution to one of these problems.

I guess he used Lean to check it?

This stuff is getting very impressive

reply
12 sats \ 2 replies \ @nathanael 5h

oh the graph is from tim urban, i finished his book yesterday

i tend to tell people that ai isn't intelligent — just as social media isn't social

reply

thank you. I did not know this was the original source of the cartoon and regret not posting a source :(

reply

the source is included in the graph (bottom right) — you're good

reply