TMBR: April 2026: Difference between revisions
Jump to navigation
Jump to search
BBµ results |
RobinCodes (talk | contribs) Updated references for consistency |
||
| Line 6: | Line 6: | ||
== BB Adjacent == | == BB Adjacent == | ||
* 3 Apr 2026: Jacob Mandelson proved the values up to BBµ(7).<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1489782558446321677]</sup> | * [[General Recursive Function]] | ||
* 9 Apr 2026: Jacob Mandelson discovered a new family of champions for BBµ(n).<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1492021428546179182]</sup> | ** 3 Apr 2026: Jacob Mandelson proved the values up to BBµ(7).<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1489782558446321677]</sup> | ||
** 9 Apr 2026: Jacob Mandelson discovered a new family of champions for BBµ(n).<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1492021428546179182]</sup> | |||
== Misc == | == Misc == | ||
* Katelyn Doucette completed [https://github.com/Laturas/FractranVisualizer a visualizer] for Fractran space-time diagrams.<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1488727841951449088 <nowiki>[ | * Katelyn Doucette completed [https://github.com/Laturas/FractranVisualizer a visualizer] for Fractran space-time diagrams.<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1488727841951449088 <nowiki>[3]</nowiki>]</sup> | ||
== Holdouts == | == Holdouts == | ||
*[[BB(6)]] | *[[BB(6)]] | ||
**Discord user sheep discovered<sup>[https://discord.com/channels/960643023006490684/1448375857046360094/1490939334092787722 <nowiki>[ | **Discord user sheep discovered<sup>[https://discord.com/channels/960643023006490684/1448375857046360094/1490939334092787722 <nowiki>[4]</nowiki>][https://discord.com/channels/960643023006490684/1448375857046360094/1490772706269069313 <nowiki>[5]</nowiki>]</sup> a new [[Cryptid]], {{TM|1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE}}, 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]]: {{TM|1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA}} | **BMO 8 was added to the [[Beaver Math Olympiad]]: {{TM|1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA}} | ||
*[[BB(7)]] | *[[BB(7)]] | ||
**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>[ | **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 holdout count to 67, with 60 informal holdouts. | ||
Revision as of 21:09, 11 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)
- 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 holdout count to 67, 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.