TMBR: 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. TODO: Write proper introductory paragraph. Important: BB(2,5) formalisation result.

Misc

• Katelyn Doucette completed a visualizer for Fractran space-time diagrams.^[1]

Holdouts

• BB(6)
  • Discord user sheep discovered 1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE (bbch), a possible cryptid similar to Space Needle.
• BB(7)
  • Further filtering by Andrew Ducharme reduced the number of holdouts from 18,036,852 to 17,823,260.^[2] (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.