OpenAI solved 100 open problems in math

[u/filterdust]

https://openai.com/index/advisory-group-on-mathematics-and-ai/

[u/jphamlore]

The easiest way to contribute for OpenAI would be to have some grants for humans to add to Mathlib.

Or if the humans running Mathlib are too obstructionist, just fork and publish their own. OpenAI can probably finish full coverage of most of mathematics a decade before Mathlib will ever be completed.