Link to the actual paper: https://www.nature.com/articles/s41586-021-04086-x

This is a twist on an old theme (just add machine learning!), where, previously, the machines would make the conjectures, and humans would prove them. In this case, it's more along the lines of the machine noticing that certain things are related, which inspires humans to prove that relationship, which eventually leads to the solution of a big, outstanding conjecture.

Here is a paper about automated conjecturing in graph theory, if you want to see the other side of the coin. No cool ML stuff, but fun nonetheless: https://www.sciencedirect.com/science/article/pii/S002437950...

From a research perspective, this is a win, and I dont want to downplay it.

Its interesting to consider this is the context of deepmind and other "commercial" AI research shops though, and how it stack up against the promises made about AI. One way to look at the headline is that researchers finally found something AI can do, and it turned out to be in some obscure area of number theory. Again, this is cool from a research perspective, connecting to disparate subjects to get a result. But if this is the kind of thing we're finding that AI is good at, what does it say about the commercial hype around it?

Yes, absolutely, this is an amazing win, and I say that as someone who studied math at the graduate level. The more drudgery we can offload to the computer, the better it is for everyone. In this case, though, the computer actually provided the equivalent of creative thought, leading to new directions toward a proof.

Personally, I've been looking around for resources on driving a proof assistant (Lean is my current favorite) using a scripting language. If anybody happens to know of any pre-made libraries that do that, preferably in Python or Ruby, that would be awesome.