Here is a thank you to the Mathlib Initiative and to @RenPhilanthropy for funding them. Lean + Mathlib folk (1) are making huge contributions to the community but also (2) are getting snowed under by the AI wave. It is important for us all to be conscientious collaborators! 馃У
Positive users praise the Mathlib Initiative's work preparing formalized math for AI and urge funding plus collaboration, while some criticize recent poor behavior by AI groups toward Lean contributors.
Without naming names, the recent behavior of AI folk w.r.t. Lean folk has been quite poor in some cases. For example, one AI group started a collaboration with some mathematicians on a formalization project, ghosted them, then later announced that they'd completed the project.
Here is a thank you to the Mathlib Initiative and to @RenPhilanthropy for funding them. Lean + Mathlib folk (1) are making huge contributions to the community but also (2) are getting snowed under by the AI wave. It is important for us all to be conscientious collaborators! 馃У
The Mathlib Initiative is doing a bunch of work to prepare for the wave of semi-automated formalized math, and we should heavily support them! The right quality standard, which they are building towards, is to have high standards only for definitions and theorem statements, but not for all proofs (proof-internal subdefinitions and lemmas can also be AI slop sometimes).
Mathlib's original standards additionally required careful design and human review for proofs as well, which is not scalable as automation ramps up.
It would be very valuable for community health and the relationship between AI safety and math if we cement better behavior! This includes funding, not just of flashy verification projects, but also the central infrastructure and tooling shared through math and CS verification.
This will require a mixture of norm adaptation and tooling, as the Lean frontend itself is not well set up for this purpose (the backend is fine).
There has been a lot of chatter about bugs in Lean, but most of it is not very precise. Broadly, we can classify bugs into three types: axioms, kernel bugs, and elaborator bugs. 馃У
It would be very valuable for community health and the relationship between AI safety and math if we cement better behavior! This includes funding, not just of flashy verification projects, but also the central infrastructure and tooling shared through math and CS verification.
Successful funding and conscientious collaboration of Lean and Mathlib will help both us at Sequent, related alignment organizations, and all applications of Lean to defensive cybersecurity (of which there are tons).
New paper with Gopal Sarma, Rachel Steratore, and Sunny Bhatt, and me surveying formal methods folk about importance and tractability of applications to AI safety. I'm excited this is out!
Here is a broader plea for people to be very ambitious about verifying software! 馃У
Here is a thank you to the Mathlib Initiative and to @RenPhilanthropy for funding them. Lean + Mathlib folk (1) are making huge contributions to the community but also (2) are getting snowed under by the AI wave. It is important for us all to be conscientious collaborators! 馃У