Proof Assistant Makes Jump to Big-League Math

Computer proof assistants have been an intriguing subplot in mathematics for years — promising to automate core aspects of the way mathematicians work, but in practice having little effect on the field. But a new result, completed in early June, has the feel of a rookie’s first hit in the big leagues: At last, a proof assistant has made a real contribution to the leading edge of mathematical…

Source