<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>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></item><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>zozbot234</author><text>&amp;gt; Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib&lt;p&gt;Yes but the bulk of the work on this project was background as well.  So the ease of use problem should be solving itself over time as more and more prereqs get filled in.&lt;p&gt;BTW, I find it interesting that mathlib is apparently also getting refactored to accommodate constructive proofs better, as part of the porting effort to Lean 4.  This might encourage more CS- and program-verification minded folks to join the effort, and maybe some folks in math-foundations too (though Lean suffers there by not being able to work with the homotopy-types axioms).</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>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></item><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>ska</author><text>&amp;gt;Something that was necessary for the success of this was years of development that had already been&lt;p&gt;For projects like this it is often very thankless work in the beginning, and can be a real grind.&lt;p&gt;You need at least one person with a vision of how cool it will be in the (poorly defined) future, and a lot of determination.</text></comment>