Hacker NewsAutomatic Textbook Formalization
https://github.com/facebookresearch/repoprover
#HackerNews #Automatic #Textbook #Formalization #Facebook #Research #Textbooks #AI #Education #Technology
Raphael APPENZELLERHalf 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/
Fractal SentienceThe formal specification. This paper develops the mathematical operators for multi-scale recursive dynamics—connecting quantum, neural, and cosmic domains through a unified formalism.
https://doi.org/10.5281/zenodo.15784341
#Mathematics #CrossScale #Formalization
https://doi.org/10.5281/zenodo.15784341
#Mathematics #CrossScale #Formalization
Part III: Mathematical Framework for Multi-Scale Recursive Dynamics: From Quantum to Cosmic Scales
Building on convergent empirical evidence documented in Parts I and II of the Universal Recursive Dynamics Series, this paper seeks to formalize universal recursive organization through unified mathematical constructs. The mathematics provide a foundation for the empirical convergence documented in Part I while enabling the cosmic extensions explored in Part II, a unified formalism for recursive phenomena from quantum to cosmological scales. All mathematical constructs are proposed as heuristic models intended to guide theoretical development, empirical testing, and computational implementation rather than function as definitive derivations. The framework strives to maintain rigorous falsification criteria while generating testable predictions that distinguish recursive from non-recursive system dynamics. v1.3.2 License changed to CC-BY 4.0 to enable full scientific dissemination. No changes to content. v1.3.1 corrects a LaTeX error that caused the word "latex" to appear at the beginning of the abstract. Moves the Addendum in front of the Appendices for series consistency. v.1.3 corrests minor unicode quotation mark errors in text only. v.1.2 adds an Aperture Addendum and a cross-referencing footnote linking to Part IV, clarifying the recursive aperture model and bridging to the series conclusion. v.1.1 adds missing Li et al. (2012) bibliographic entry that caused (?Miroshnikova et al., 2023) citation error.
sayzardfly51fly (@fly51fly)
J. Urban의 논문은 단기간(2주) 동안 13만 줄 규모의 형식적 위상수학(formal topology)을 자동 형식화(autoformalization)로 생성한 작업을 보고합니다. 비용과 복잡도를 낮춘 간단한 방법을 제안해 누구나 자동 형식화에 접근할 수 있게 하는 접근법과 실험 결과를 제시하며 정리된 데이터셋과 파이프라인을 공개합니다 (arXiv:2601.03298).
https://x.com/fly51fly/status/2013735633425146080
#autoformalization #formalization #theoremproving #automatedreasoning
Bjørn SætrevikWe'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
ThomasRobert 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.
Tom de JongI'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 🙂
Formalizing equivalences without tears
This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. The techniques are illustrated by proving a basic result in synthetic homotopy theory.
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
Programming Languages DelftMaster 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."
#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."