DeepMind cracks 'knot' conjecture that bedeviled mathematicians for decades
livescience.com
livescience.com
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...
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?
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.