A new #Lean formalization project led by Alex Kontorovich and myself has just been announced to formalize the proof of the prime number theorem, as well as much of the attendant supporting machinery in complex analysis and analytic number theory, with the plan to then go onward and establish further results such as the Chebotarev density theorem. The repository for the project (including the blueprint) is at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd , and discussion will take place at this Zulip stream: https://leanprover.zulipchat.com/#narrow/stream/423402-PrimeNumberTheorem.2B
A couple months ago, another mathematician contacted me and two of my co-authors (Green and Manners) regarding a minor mathematical misprint in one of our papers. Normally this is quite a routine occurrence, but it caused a surprising amount of existential panic on my part because I thought it involved the #PFR paper that I had run a #Lean formalization project in. As it turned out, though, the misprint involved a previous paper, in a portion that was not formalized in Lean. So all was well; we thanked the mathematician and updated the paper accordingly.
But yesterday, we received referee reports for the PFR paper that was formalized in Lean, and one of the referees did actually spot a genuine mathematical typo (specifically, the expression H[A]-H[B] appearing in (A.22) of https://arxiv.org/abs/2311.05762 should be H[A]+H[B]). So this again created a moment of panic - how could Lean have missed this?
After reviewing the Github history for the blueprint, I found that when I transcribed the proof from the paper to blueprint form, I had unwittingly corrected this typo (see Equation (9) of https://teorth.github.io/pfr/blueprint/sect0003.html in the proof of Lemma 3.23) without noticing that the typo was present in the original source paper. This lemma was then formalized by other contributors without difficulty. I don't remember my actual thought process during the transcription, but I imagine it is similar to how when reading in one's native language, one can often autocorrect spelling and grammar errors in the text without even noticing that one is doing so. Still, the experience gives me just a little pause regarding how confident one can be in the 100% correctness of a paper that was formalized...
We are organizing the FP Dag aka Dutch Functional Programming Day on Friday the 5th of January in Delft. People from neighboring countries are also very welcome to join!
The (soft) registration deadline is on the 22th of December (next Friday), so get your tickets soon!
Published: On the Evilness of Feature Branching - What about Code Reviews?
How do we do code reviews when there are no version control branches?
We have 4 options at our disposal. And the first one might be surprising. What about no code reviews? Heuh 😳 It might work, you know. Maybe not for regulated industries.
I've implemented functional induction theorems in Lean, shipping with the upcoming version 4.8.0, and wrote a tutorial-style blog post about it: https://lean-lang.org/blog/2024-5-17-functional-induction/
(h't to David Christiansen for the tooling behind the hover features.) #lean#leanlang
Hi folks! I have a new article up on LinkedIn called, "I'm Not Just an Agile Coach!", in which I explain why I don't completely fit the common perception of what an Agile Coach is, and how I have much more to offer! #Agile#Coaching#XP#Lean#DevOps#ContinuousDelivery
The #Bootstrapping#Startup Operating System
Nice post from Ash Maurya, the old good idea of running #lean always apply. Getting #customer- funded not #VC-funded is better:
Someone once said that laziness is what kept #Haskell pure, and that's the actually relevant feature. This makes we wonder: will theorem proving languages like #lean, where logical consistency is what keeps them pure, deliver the same elegant experience, while avoiding some downsides of laziness (complex runtime, complicated performance characteristics)?
Tomorrow is already the deadline for the third edition of #WITS, the Workshop on the Implementation of Type Systems, colocated with #POPL 2024 in London. The page limit is one page, but just a single-paragraph abstract with an interesting idea for a talk is also very welcome! In particular contributors to #Haskell#OCaml#Rust#Scala#Coq#Lean#Agda#Idris#Cedille#Arend#CoolTT and even #TypeScript are warmly invited to give a talk about their experiences with implementing type systems.
@andreclaassen das #fediverse ist so voller verschiedener sachen, #firefish#gotosocial#castopod da kann man soviel ausprobieren von motivierten leuten programmiertes, da hab ich persoenlich gar keinen bedarf zu schauen, was die milliardaere des planetens so programmieren lassen.
wir sind zwar nicht mehr, aber vielleicht genug ;)