TMBR: April 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) Added reference link to Sheep discovering the Cryptid, added summary text of this month. |
RobinCodes (talk | contribs) Change sheep to lowercase. |
||
| Line 3: | Line 3: | ||
''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 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).'' | ||
[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for April 2026. This month, a new [[Cryptid]] was discovered in [[BB(6)]] by Discord user | [[:Category:This Month in Beaver Research|This Month in Beaver Research]] for April 2026. This month, a new [[Cryptid]] was discovered in [[BB(6)]] by Discord user sheep. 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)]]. | ||
== Misc == | == Misc == | ||
Revision as of 19:23, 9 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. 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).
Misc
- Katelyn Doucette completed a visualizer for Fractran space-time diagrams.[1]
Holdouts
- BB(6)
- Discord user Sheep discovered[1][2] 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).
- Discord user Sheep discovered[1][2] a new Cryptid,
- BB(7)
- Further filtering by Andrew Ducharme reduced the number of holdouts from 18,036,852 to 17,823,260.[3] (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.