<story><title>&apos;A-team&apos; of math proves a critical link between addition and sets</title><url>https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/</url></story><parent_chain><item><author>blowski</author><text>The maths goes over my head, but this paragraph was very interesting:&lt;p&gt;&amp;gt; Tao then kicked off an effort to formalize the proof in Lean, a programming language that helps mathematicians verify theorems. In just a few weeks, that effort succeeded. Early Tuesday morning of December 5, Tao announced that Lean had proved the conjecture without any “sorrys” — the standard statement that appears when the computer can’t verify a certain step. This is the highest-profile use of such verification tools since 2021, and marks an inflection point in the ways mathematicians write proofs in terms a computer can understand. If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, said Gowers.</text></item></parent_chain><comment><author>kmill</author><text>I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support).&lt;p&gt;It&amp;#x27;s exciting to see how quickly the work was done, but it&amp;#x27;s worth keeping in mind that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users.&lt;p&gt;There aren&amp;#x27;t enough experienced Lean users to go around yet for any old project, so Gowers&amp;#x27;s point about ease of use is an important one.&lt;p&gt;Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It&amp;#x27;s reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.</text></comment>
<story><title>&apos;A-team&apos; of math proves a critical link between addition and sets</title><url>https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/</url></story><parent_chain><item><author>blowski</author><text>The maths goes over my head, but this paragraph was very interesting:&lt;p&gt;&amp;gt; Tao then kicked off an effort to formalize the proof in Lean, a programming language that helps mathematicians verify theorems. In just a few weeks, that effort succeeded. Early Tuesday morning of December 5, Tao announced that Lean had proved the conjecture without any “sorrys” — the standard statement that appears when the computer can’t verify a certain step. This is the highest-profile use of such verification tools since 2021, and marks an inflection point in the ways mathematicians write proofs in terms a computer can understand. If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, said Gowers.</text></item></parent_chain><comment><author>spadufed</author><text>If anybody&amp;#x27;s interested in learning more about Lean, he&amp;#x27;s been posting his experiences with the project over at @tao@mathstodon.xyz</text></comment>