Recently I got interested in #Lean proof assistant, so naturally I went out to see what parts of my field - set theory - has been formalized with Lean.
Turns out the independence of the Continuum Hypothesis have been formalized. This video gives an interesting overview.
https://www.youtube.com/watch?v=4LkumFrg68s
The past two months, I helped coordinate the "Phase Transitions..." research semester programme at CWI (https://www.cwi.nl/en/events/research-semester-programmes/phasecap-phase-transitions-in-combinatorics-algorithms-probability/). It ended last Friday, and still I feel "hungover" from the intensive blur of activities/developments/ideas. Very grateful to my team --Feri, Jop, Serte, Carla, Noela, Guus-- we did it!
In parallel, during the same two months, after the dawn of recognition of what has arrived (after a tip from Jeroen), I underwent a kind of phase transition myself. Avowed refusenik in March (see https://mathstodon.xyz/@kangmeister/115252549665766971); an "anti-Gemini" research working group in April; compulsive button-pressing in May. (And yes, I *know* it is easy to set it up for pressing fewer buttons...)
That poetic part of me (or whatever remains of it) is allured by the term, "cognitive surrender", if only to help in my search for the right words to describe the sharp changes underway in various facets of mathematical life/growth.
#CWI #combinatorics #algorithms #probability #conferences #generativeAI #formalization #lean #scientificpublishing
Automatic Textbook Formalization
https://github.com/facebookresearch/repoprover
#HackerNews #Automatic #Textbook #Formalization #Facebook #Research #Textbooks #AI #Education #Technology
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/
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.
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.
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 🙂
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
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."
#Agda #formalization #patternmatching #dependenttypes #master
Ur Ya'ar
Ross Kang
Hacker News
Raphael APPENZELLER
Fractal Sentience
Bjørn Sætrevik
Thomas
Tom de Jong
Programming Languages Delft