TMBR: April 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) Fixed reference format |
RobinCodes (talk | contribs) Added BB(2,5) formalisation |
||
| 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. | [[:Category:This Month in Beaver Research|This Month in Beaver Research]] for April 2026. TODO: Write proper introductory paragraph. Important: BB(2,5) formalisation result. | ||
== 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>[1]</nowiki>]</sup> | * Katelyn Doucette completed [https://github.com/Laturas/FractranVisualizer a visualizer] for Fractran space-time diagrams.<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1488727841951449088 <nowiki>[1]</nowiki>]</sup> | ||
== Holdouts == | |||
* [[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.ai/ 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. | |||
[[Category:This Month in Beaver Research|2026-04]] | [[Category:This Month in Beaver Research|2026-04]] | ||
Revision as of 14:46, 1 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(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.