AI Is Coming for Mathematics

The first mathematical theorem proved with the help of a computational tool? Does anybody know what that is? I'll give you a hint. It was, it was proved in 1976. A proof assistant system called Lean uses AI inspired logic to do more brute force for mathematicians. And right now, it's actively being used by mathematicians and purists who are saying we wouldn't use it otherwise.