NotAwfulTech

Other Scott has clarified his position on citational standards in a comment on his blog:

Wow, that’s really cool; I hadn’t seen [a recent independence result]. Thanks! Given all the recent claims there have been to lower the n for which BB(n) is known to be independent of ZFC, though, I would like to establish a ground rule that a claim needs either a prose writeup explaining what was done or independent verification of its correctness, ideally both but certainly at least one, rather than just someone’s GitHub repo.

In contrast, the Gauge's standard is that a claim needs reproducible computable artifacts as supporting evidence, with inline comments serving as sufficient documentation for those already well-versed in the topic, and any supporting papers or blog posts are merely a nicety for explaining the topic and construction to the mathematical community and laity at large. If a claim is not sufficiently strong then we should introduce more computational evidence to settle the question at hand.

For example, Leng 2024 gives a construction in Lean 4. If this is not strong enough then the Gauge could be configured to compile a Nix-friendly Lean 4 and expend some compute in CI to verify the proof, so that the book only builds if Leng's proof is valid. Further critique would focus on what Leng actually proved in terms of their Lean 4 code. Other Scott isn't convinced by this, so it's not part of the story that they will tell.

This isn't my field, but it looks like a neat project!

this is going to take up the rest of my evening, now i'm reading about the Pólya conjecture for the first time

this rules 💗

Hell yeah,, thanks for doing this