A few times I have told the anecdote that the singly most baffling thing I ever saw in a code review — not the most insecure, just the most “how could a real programmer have written this? how could this ever make sense?” thing — was simply a C++ variable “number_of_trucks” … declared as float. Unambiguously referring to real physical trucks in a fleet.

Reader, it’s been over ten years and I am blowing the gods damn whistle. I had edited that story to protect the guilty: the variable was named number_of_planes. It was shipped by a company whose name begins with “B” and rhymes with “GOING out of business.”

The #Lean4 project to formalize the proof of the Polynomial Freiman-Ruzsa conjecture has succeeded after three weeks, with the dependency graph completely covered in a lovely shade of green: https://teorth.github.io/pfr/blueprint/dep_graph_document.html , and the Lean compiler reporting that the conjecture follows from standard axioms.

More discussion on the project can be found at https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Project.20completed!.20.20Thoughts.20and.20reflections.3F