https://wiki.bbchallenge.org/w/index.php?action=history&feed=atom&title=TMBR%3A_April_2026
TMBR: April 2026 - Revision history
2026-05-01T02:59:42Z
Revision history for this page on the wiki
MediaWiki 1.43.5
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7359&oldid=prev
Polygon: /* Holdouts */ updated BB(2,7)
2026-04-30T18:09:19Z
<p><span class="autocomment">Holdouts: </span> updated BB(2,7)</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 18:09, 30 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l84">Line 84:</td>
<td colspan="2" class="diff-lineno">Line 84:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Andrew Ducharme reduced the number of holdouts from 545,005 to '''536,112''' via Enumerate.py, a '''1.63%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1491652128123388026 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1495650803967463464 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1497280483275575347 <nowiki>[TODO]</nowiki>]</sup></div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Andrew Ducharme reduced the number of holdouts from 545,005 to '''536,112''' via Enumerate.py, a '''1.63%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1491652128123388026 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1495650803967463464 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1497280483275575347 <nowiki>[TODO]</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(2,7)]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(2,7)]]</div></td></tr>
<tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>** Terry Ligocki enumerated <del style="font-weight: bold; text-decoration: none;">110K </del>more subtasks, increasing the number of holdouts to '''<del style="font-weight: bold; text-decoration: none;">660</del>,<del style="font-weight: bold; text-decoration: none;">441</del>,<del style="font-weight: bold; text-decoration: none;">047</del>'''. A total of <del style="font-weight: bold; text-decoration: none;">210K </del>subtasks out of the 1 million subtasks (or '''<del style="font-weight: bold; text-decoration: none;">21</del>%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[7]</nowiki>]</sup></div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>** Terry Ligocki enumerated <ins style="font-weight: bold; text-decoration: none;">120K </ins>more subtasks, increasing the number of holdouts to '''<ins style="font-weight: bold; text-decoration: none;">687</ins>,<ins style="font-weight: bold; text-decoration: none;">123</ins>,<ins style="font-weight: bold; text-decoration: none;">946</ins>'''. A total of <ins style="font-weight: bold; text-decoration: none;">220K </ins>subtasks out of the 1 million subtasks (or '''<ins style="font-weight: bold; text-decoration: none;">22</ins>%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[7]</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:This Month in Beaver Research|2026-04]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:This Month in Beaver Research|2026-04]]</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7358:rev-7359:php=table -->
</table>
Polygon
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7358&oldid=prev
Polygon: /* Holdouts */ linked Phase 3
2026-04-30T17:53:53Z
<p><span class="autocomment">Holdouts: </span> linked Phase 3</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 17:53, 30 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l76">Line 76:</td>
<td colspan="2" class="diff-lineno">Line 76:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(3,4)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(3,4)]]:</div></td></tr>
<tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>**Andrew ducharme began Phase 3, reducing the holdout count from 12,435,284 to '''12,049,358''' (a '''3.10%''' reduction) with mxdys's FAR decider.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>**Andrew ducharme began <ins style="font-weight: bold; text-decoration: none;">[[BB(3,4)#Phase 3|</ins>Phase 3<ins style="font-weight: bold; text-decoration: none;">]]</ins>, reducing the holdout count from 12,435,284 to '''12,049,358''' (a '''3.10%''' reduction) with mxdys's FAR decider.</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7357:rev-7358:php=table -->
</table>
Polygon
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7357&oldid=prev
Polygon: /* Holdouts */ mentioned Phase 3 in text
2026-04-30T17:53:11Z
<p><span class="autocomment">Holdouts: </span> mentioned Phase 3 in text</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 17:53, 30 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l76">Line 76:</td>
<td colspan="2" class="diff-lineno">Line 76:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(3,4)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(3,4)]]:</div></td></tr>
<tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>**Andrew ducharme <del style="font-weight: bold; text-decoration: none;">reduced </del>the holdout count from 12,435,284 to '''12,049,358''' (a '''3.10%''' reduction) with mxdys's FAR decider.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>**Andrew ducharme <ins style="font-weight: bold; text-decoration: none;">began Phase 3, reducing </ins>the holdout count from 12,435,284 to '''12,049,358''' (a '''3.10%''' reduction) with mxdys's FAR decider.</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7356:rev-7357:php=table -->
</table>
Polygon
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7356&oldid=prev
Polygon: Added holdout reduction table
2026-04-30T17:51:58Z
<p>Added holdout reduction table</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 17:51, 30 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l18">Line 18:</td>
<td colspan="2" class="diff-lineno">Line 18:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Holdouts ==</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Holdouts ==</div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">{| class="wikitable"</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|+BB Holdout Reduction by Domain</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">!Domain</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">!Previous Holdout Count</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">!New Holdout Count</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">!Holdout Reduction</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">!% Reduction</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|[[BB(6)]]</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|1161</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|1104</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|57</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|4.91%</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|[[BB(7)]]</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|18,036,852</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|17,823,260</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|213,592</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|1.18%</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|[[BB(4,3)]]</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|9,401,447</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|5,641,006</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|3,760,441</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|40.00%</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|[[BB(3,4)]]</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|12,435,284</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|12,049,358</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|385,926</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|3.10%</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|[[BB(2,5)]]</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|69</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|66</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|3</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|4.35%</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|[[BB(2,6)]]</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|545,005</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|536,112</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|8,893</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|1.63%</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|}</ins></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(6)]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(6)]]</div></td></tr>
<tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l32">Line 32:</td>
<td colspan="2" class="diff-lineno">Line 76:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(3,4)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(3,4)]]:</div></td></tr>
<tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>**Andrew ducharme reduced the holdout count from 12,435,284 to '''12,049,358''' (a 3.10% reduction) with mxdys's FAR decider.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>**Andrew ducharme reduced the holdout count from 12,435,284 to '''12,049,358''' (a <ins style="font-weight: bold; text-decoration: none;">'''</ins>3.10%<ins style="font-weight: bold; text-decoration: none;">''' </ins>reduction) with mxdys's FAR decider.</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7355:rev-7356:php=table -->
</table>
Polygon
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7355&oldid=prev
Polygon: /* Holdouts */ added BB(3,4) holdout reduction
2026-04-30T17:45:09Z
<p><span class="autocomment">Holdouts: </span> added BB(3,4) holdout reduction</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 17:45, 30 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l31">Line 31:</td>
<td colspan="2" class="diff-lineno">Line 31:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(4,3)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(4,3)]]:</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** In [[BB(4,3)#Stage 3|phase 2 stage 3]], Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* [[BB(3,4)]]:</ins></div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">**Andrew ducharme reduced the holdout count from 12,435,284 to '''12,049,358''' (a 3.10% reduction) with mxdys's FAR decider.</ins></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7342:rev-7355:php=table -->
</table>
Polygon
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7342&oldid=prev
Polygon: /* Holdouts */ Added new holdouts list
2026-04-29T15:48:00Z
<p><span class="autocomment">Holdouts: </span> Added new holdouts list</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 15:48, 29 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l25">Line 25:</td>
<td colspan="2" class="diff-lineno">Line 25:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Discord user The_Real_Fourious_Banana [https://discord.com/channels/960643023006490684/1477591686514212894/1495412160237539338 simulated another TM] to 1e15, reducing the 1e14 holdout count to 169 and the 1e15 holdout count to 235.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Discord user The_Real_Fourious_Banana [https://discord.com/channels/960643023006490684/1477591686514212894/1495412160237539338 simulated another TM] to 1e15, reducing the 1e14 holdout count to 169 and the 1e15 holdout count to 235.</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1497651809773289552 released] a new holdouts list of '''1119''' machines, the reduction mostly (except for [https://discord.com/channels/960643023006490684/1239205785913790465/1497668636117176520 one TM]) came from new equivalences.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1497651809773289552 released] a new holdouts list of '''1119''' machines, the reduction mostly (except for [https://discord.com/channels/960643023006490684/1239205785913790465/1497668636117176520 one TM]) came from new equivalences.</div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">**Later, mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1499000732236382358 released] a new holdouts list of '''1104''' machines where more equivalence classes have been merged.</ins></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**TODO: Add BB6 holdouts decrease graph in 2026: https://discord.com/channels/960643023006490684/1239205785913790465/1492615938824999034</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**TODO: Add BB6 holdouts decrease graph in 2026: https://discord.com/channels/960643023006490684/1239205785913790465/1492615938824999034</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(7)]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(7)]]</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7322:rev-7342:php=table -->
</table>
Polygon
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7322&oldid=prev
Tjligocki: /* Holdouts */ Removed extra space
2026-04-27T05:33:28Z
<p><span class="autocomment">Holdouts: </span> Removed extra space</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 05:33, 27 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l37">Line 37:</td>
<td colspan="2" class="diff-lineno">Line 37:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Andrew Ducharme reduced the number of holdouts from 545,005 to '''536,112''' via Enumerate.py, a '''1.63%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1491652128123388026 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1495650803967463464 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1497280483275575347 <nowiki>[TODO]</nowiki>]</sup></div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Andrew Ducharme reduced the number of holdouts from 545,005 to '''536,112''' via Enumerate.py, a '''1.63%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1491652128123388026 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1495650803967463464 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1497280483275575347 <nowiki>[TODO]</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(2,7)]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(2,7)]]</div></td></tr>
<tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>** Terry Ligocki enumerated 110K more subtasks, increasing the number of holdouts to '''660,441,047''' . A total of 210K subtasks out of the 1 million subtasks (or '''21%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[7]</nowiki>]</sup></div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>** Terry Ligocki enumerated 110K more subtasks, increasing the number of holdouts to '''660,441,047'''. A total of 210K subtasks out of the 1 million subtasks (or '''21%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[7]</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:This Month in Beaver Research|2026-04]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:This Month in Beaver Research|2026-04]]</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7321:rev-7322:php=table -->
</table>
Tjligocki
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7321&oldid=prev
Tjligocki: /* Holdouts */ Updated BB(2,7) progress
2026-04-27T05:32:56Z
<p><span class="autocomment">Holdouts: </span> Updated BB(2,7) progress</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 05:32, 27 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l37">Line 37:</td>
<td colspan="2" class="diff-lineno">Line 37:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Andrew Ducharme reduced the number of holdouts from 545,005 to '''536,112''' via Enumerate.py, a '''1.63%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1491652128123388026 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1495650803967463464 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1497280483275575347 <nowiki>[TODO]</nowiki>]</sup></div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Andrew Ducharme reduced the number of holdouts from 545,005 to '''536,112''' via Enumerate.py, a '''1.63%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1491652128123388026 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1495650803967463464 <nowiki>[TODO]</nowiki>][https://discord.com/channels/960643023006490684/1084047886494470185/1497280483275575347 <nowiki>[TODO]</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(2,7)]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(2,7)]]</div></td></tr>
<tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>** Terry Ligocki enumerated <del style="font-weight: bold; text-decoration: none;">100K </del>more subtasks, increasing the number of holdouts to '''<del style="font-weight: bold; text-decoration: none;">632</del>,<del style="font-weight: bold; text-decoration: none;">436</del>,<del style="font-weight: bold; text-decoration: none;">144</del>'''. A total of <del style="font-weight: bold; text-decoration: none;">200K </del>subtasks out of the 1 million subtasks (or '''<del style="font-weight: bold; text-decoration: none;">20</del>%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[7]</nowiki>]</sup></div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>** Terry Ligocki enumerated <ins style="font-weight: bold; text-decoration: none;">110K </ins>more subtasks, increasing the number of holdouts to <ins style="font-weight: bold; text-decoration: none;"> </ins>'''<ins style="font-weight: bold; text-decoration: none;">660</ins>,<ins style="font-weight: bold; text-decoration: none;">441</ins>,<ins style="font-weight: bold; text-decoration: none;">047</ins>''' . A total of <ins style="font-weight: bold; text-decoration: none;">210K </ins>subtasks out of the 1 million subtasks (or '''<ins style="font-weight: bold; text-decoration: none;">21</ins>%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[7]</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:This Month in Beaver Research|2026-04]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>[[Category:This Month in Beaver Research|2026-04]]</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7317:rev-7321:php=table -->
</table>
Tjligocki
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7317&oldid=prev
Polygon: /* Holdouts */ Linked stage 3
2026-04-26T18:42:54Z
<p><span class="autocomment">Holdouts: </span> Linked stage 3</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 18:42, 26 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l29">Line 29:</td>
<td colspan="2" class="diff-lineno">Line 29:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Further filtering by Andrew Ducharme reduced the number of holdouts from 18,036,852 to '''17,823,260'''.<sup>[https://discord.com/channels/960643023006490684/1369339127652159509/1490808711952728235 <nowiki>[6]</nowiki>]</sup> (A '''1.18%''' reduction)</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Further filtering by Andrew Ducharme reduced the number of holdouts from 18,036,852 to '''17,823,260'''.<sup>[https://discord.com/channels/960643023006490684/1369339127652159509/1490808711952728235 <nowiki>[6]</nowiki>]</sup> (A '''1.18%''' reduction)</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(4,3)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(4,3)]]:</div></td></tr>
<tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>** In phase 2 stage 3, Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>** In <ins style="font-weight: bold; text-decoration: none;">[[BB(4,3)#Stage 3|</ins>phase 2 stage 3<ins style="font-weight: bold; text-decoration: none;">]]</ins>, Andrew Ducharme reduced the number of holdouts from 9,401,447 to '''5,641,006''', a '''40.00%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1497715882049147143 <nowiki>TODO</nowiki>]</sup></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [[BB(2,5)]]:</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>** On 1 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1488737894943166604 Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution], which he created using [https://aristotle.harmonic.fun/ Aristotle AI]. Then [https://discord.com/channels/960643023006490684/1259770421046411285/1488898494386274374 mxdys formalised the result] in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7309:rev-7317:php=table -->
</table>
Polygon
https://wiki.bbchallenge.org/w/index.php?title=TMBR:_April_2026&diff=7309&oldid=prev
Polygon: /* Holdouts */ Added new BB(6) holdouts list
2026-04-26T08:55:51Z
<p><span class="autocomment">Holdouts: </span> Added new BB(6) holdouts list</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en">
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Revision as of 08:55, 26 April 2026</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l24">Line 24:</td>
<td colspan="2" class="diff-lineno">Line 24:</td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Alistaire [https://discord.com/channels/960643023006490684/1477591686514212894/1490470766116864291 simulated a machine] to 1e15.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Alistaire [https://discord.com/channels/960643023006490684/1477591686514212894/1490470766116864291 simulated a machine] to 1e15.</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Discord user The_Real_Fourious_Banana [https://discord.com/channels/960643023006490684/1477591686514212894/1495412160237539338 simulated another TM] to 1e15, reducing the 1e14 holdout count to 169 and the 1e15 holdout count to 235.</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**Discord user The_Real_Fourious_Banana [https://discord.com/channels/960643023006490684/1477591686514212894/1495412160237539338 simulated another TM] to 1e15, reducing the 1e14 holdout count to 169 and the 1e15 holdout count to 235.</div></td></tr>
<tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">**mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1497651809773289552 released] a new holdouts list of '''1119''' machines, the reduction mostly (except for [https://discord.com/channels/960643023006490684/1239205785913790465/1497668636117176520 one TM]) came from new equivalences.</ins></div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**TODO: Add BB6 holdouts decrease graph in 2026: https://discord.com/channels/960643023006490684/1239205785913790465/1492615938824999034</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>**TODO: Add BB6 holdouts decrease graph in 2026: https://discord.com/channels/960643023006490684/1239205785913790465/1492615938824999034</div></td></tr>
<tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(7)]]</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>*[[BB(7)]]</div></td></tr>
<!-- diff cache key mediawiki:diff:1.41:old-7300:rev-7309:php=table -->
</table>
Polygon