From the blog post: ... ... I cannot verify any of this and there are no mainstream news articles, but it seems big if true.
From the blog post:
[W]e are pleased to announce that with Gauss, we have completed the project [formalize the strong Prime Number Theorem in Lean] after three weeks of effort. Gauss can work autonomously for hours, dramatically compressing the labor previously reserved for top formalization experts. Along the way, Gauss formalized the key missing results in complex analysis, which opens up future initiatives previously considered unapproachable.
Using Gauss we produced ~25,000 lines of Lean code, comprising over 1,000 theorems and definitions. Formal proofs of this scale have historically been major milestones, often the culmination of multi-year efforts. The largest singular formalization projects in history — career-defining efforts, which can span more than a decade — are only an order of magnitude larger at up to 500,000 lines of code. Lean’s standard mathematical library, Mathlib, is an order of magnitude beyond that, at around 2,000,000 lines of code, comprising 350,000 Lean theorems and definitions, and developed by over 600 human contributors over eight years.
...
We will begin deploying our technology to make it useful to working mathematicians and proof engineers. Presently, we are in contact with a select group of mathematicians for beta testing.
...
Our results represent the first steps towards formalization at an unprecedented scale. Gauss will soon dramatically compress the time to complete massive initiatives. With further algorithmic improvements, we aim to increase the sum total of formal code by 2-3 orders of magnitude in the coming 12 months.
I cannot verify any of this and there are no mainstream news articles, but it seems big if true.
From the blog post:
...
...
I cannot verify any of this and there are no mainstream news articles, but it seems big if true.