TMBR: April 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) Added TODO |
RobinCodes (talk | contribs) m Better wording |
||
| Line 24: | Line 24: | ||
**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) | **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) | ||
* [[BB(2,5)]]: | * [[BB(2,5)]]: | ||
** 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 holdout count to 67, with 60 informal holdouts. | ** 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. | ||
** On 2 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1489095097373954199 mxdys solved] [[Beaver Math Olympiad#Solved problems|BMO 3]] variant {{TM|1RB0RA3LA4LA2RA_2LB3LA---4RA3RB}} using an LLM, reducing the formal holdout count to 66. The proofs for BMO 3 and its variant are available at https://github.com/ccz181078/busycoq/blob/BB6/verify/BMO3.v. | ** On 2 April 2026, [https://discord.com/channels/960643023006490684/1259770421046411285/1489095097373954199 mxdys solved] [[Beaver Math Olympiad#Solved problems|BMO 3]] variant {{TM|1RB0RA3LA4LA2RA_2LB3LA---4RA3RB}} using an LLM, reducing the formal holdout count to 66. The proofs for BMO 3 and its variant are available at https://github.com/ccz181078/busycoq/blob/BB6/verify/BMO3.v. | ||
*[[BB(2,6)]] | *[[BB(2,6)]] | ||
Revision as of 06:11, 12 April 2026
| Prev: March 2026 | This Month in Beaver Research | Next: May 2026 |
This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).
This Month in Beaver Research for April 2026. This month, a new Cryptid was discovered in BB(6) by Discord user sheep, and BMO 8 was added to BMO. Two informally proven machines were formalised into Rocq in BB(2,5), and Katelyn Doucette created a visualizer for Fractran space-time diagrams. We also shot below 18 million holdouts for BB(7).
BB Adjacent
Misc
- Katelyn Doucette completed a visualizer for Fractran space-time diagrams.[3]
Holdouts
- BB(6)
- Discord user sheep discovered[4][5] a new Cryptid,
1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE(bbch), similar to Space Needle. A classification of Cryptids is now being worked on, where this machine, for example, could belong to a class of Needles (along with Space Needle). - BMO 8 was added to the Beaver Math Olympiad:
1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA(bbch) - TODO: Add BB6 holdouts decrease graph in 2026: https://discord.com/channels/960643023006490684/1239205785913790465/1492615938824999034
- Discord user sheep discovered[4][5] a new Cryptid,
- BB(7)
- Further filtering by Andrew Ducharme reduced the number of holdouts from 18,036,852 to 17,823,260.[6] (A 1.18% reduction)
- BB(2,5):
- On 1 April 2026, Discord user mammillaria shared a Lean formalisation of the BMO 3 problem and its solution, which he created using Aristotle AI. Then mxdys formalised the result in Rocq using LLMs, reducing the formal holdout count to 67, still with 60 informal holdouts.
- On 2 April 2026, mxdys solved BMO 3 variant
1RB0RA3LA4LA2RA_2LB3LA---4RA3RB(bbch) using an LLM, reducing the formal holdout count to 66. The proofs for BMO 3 and its variant are available at https://github.com/ccz181078/busycoq/blob/BB6/verify/BMO3.v.
- BB(2,6)
- Andrew Ducharme reduced the number of holdouts from 545,005 to 542,325 via Enumerate.py, a 0.49% reduction.