Half a year ago, I filled in some sorry's for the massive project [1] to formalize the Fields-medal winning proof that sphere packing in dimension 8 is optimized by the E8-lattice. Last week it was announced that all remaining sorry's were filled by Gauss, an autoformalization agent. Gauss was able to build on the blueprint and other scaffolding built by the community. A few days later, Gauss also formalized the proof in dimension 24, this time working directly from the published paper, without mayor community input [3].
Since Lean verifies the generated proofs, hallucinations are not a problem.
The community now processes the generated proofs to make sure it satisfies the community standards and remains usable in the future [2].

[1] https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/

[2] https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Sphere.20Packing.20Milestone/with/575354368

[3] https://www.math.inc/sphere-packing

#Lean #spherepacking #gauss #formalization

fly51fly (@fly51fly)

J. Urban의 논문은 단기간(2주) 동안 13만 줄 규모의 형식적 위상수학(formal topology)을 자동 형식화(autoformalization)로 생성한 작업을 보고합니다. 비용과 복잡도를 낮춘 간단한 방법을 제안해 누구나 자동 형식화에 접근할 수 있게 하는 접근법과 실험 결과를 제시하며 정리된 데이터셋과 파이프라인을 공개합니다 (arXiv:2601.03298).

https://x.com/fly51fly/status/2013735633425146080

#autoformalization #formalization #theoremproving #automatedreasoning

We're working on a tool for standardizing hypothesis formulation. We've put together a bibliography of previous work on the topic. Are we missing any important papers?

Feel free to edit or comment: https://docs.google.com/document/d/1fJeVJZaX1v8Cmw8ibDzq0WtUolSQ8ZcPyg-kafFQEf8/edit?usp=sharing

#hypothesis #HypothesisStandardization #hypothesizer #formalization #NHST #TheoryDevelopment #OpenScience @openscience

Robert Rosen's approach of grounding formalization in science in the ultimate formalization, math, is as self-similar as thinking about thought.

His use of "category theory" provides a mathematical analogy to analogies.

I must confess that I need a lot of time to understand his writings - I keep learning new things every time I read it again.

#RobertRosen #Formalization #categorytheory

I'm happy to report that my expository note (https://arxiv.org/abs/2408.11501), which has previously been kindly mentioned on here by @ecavallo and @jonmsterling, has been accepted to the TYPES 2024 post-proceedings 🙂

#typetheory #formalization

Call for Papers
16th International Conference on Interactive Theorem Proving — ITP'25

Reykjavik, Iceland
27 September – 3 October 2025

https://icetcs.github.io/frocos-itp-tableaux25/itp/

ITP is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics.

- Abstract submission deadline: 12 March 2025
- Paper submission deadline: 19 March 2025
- Author notification: 23 May 2025
- Camera-ready copy due: 27 June 2025

#formalization #theoremproving #proofassistants #verification #CfP

Master thesis by Kayleigh Lieverse: A Generic Translation from Case Trees to Eliminators.

"We present [..] a type-safe, correct-by construction, generic definition of case trees and an evaluation function that, given an interpretation of such a case tree and an interpretation of the telescope of function arguments, evaluates the output term of the function using only eliminators."

https://repository.tudelft.nl/islandora/object/uuid%3Ae91ef1ea-942e-4f11-a1c4-bb82f444aaed?collection=education

#Agda #formalization #patternmatching #dependenttypes #master

Master thesis by Eben Rogers: Replication and formalization of (Co)Church encoded shortcut fusion.

"This thesis explores shortcut fusion using (Co)Church encodings based on the work of Harper (2011), focusing on two questions: What is needed to reliably achieve fusion in Haskell, and the correctness of these transformations through a formalization in Agda."

https://repository.tudelft.nl/islandora/object/uuid:7474b56a-345c-42b7-8d07-e7163d1bde05?collection=education

#Agda #Haskell #optimization #formalization #master

I’ve been thinking about formalization of maths a bit and for what I usually do in algebra and combinatorics this all seems rather straightforward albeit time consuming.

But then I’m reading a topology book where the proofs go like: Imagine a 4d-ball of clay where push your finger in to form 3 openings with this and that property and then identify the 3d-boundary of the inside of hole 1 with …

Will it be possible to formalize this? Will we discover many errors?

#math #formalization