User:Hakerh400/Formalization

In this subpage we list the formalization projects led by User:Hakerh400. All projects are in Lean 4. We never use AI in the process of formalization.

We divide formalization projects into three lists: finished, active and planned.

A project is finished if it has been finalized in the sense that we have successfully proved all relevant theorems that we intended to prove. We may perform chore updates on finished projects, or add a few utility theorems, but the core idea is already formalized.

A project is active if there is an ongoing formalization effort towards the final theorems that we intended to formalize.

A project is planned if we want to formalize some theory, but we haven't figured out yet the best approach to do so. Once we have a clear idea how to approach some formalization project, we move it from planned to active.

Finished projects

• Hash map / hash set: [1] [2] We reused some of the hash map internals from Lean, but we also proved substantial amount of theorems that are not in Lean.
• Digits: [3] A library for reasoning about digits of natural numebrs.
• Digital root: [4] We formally verified properties of wikipedia:Digital root in arbitrary number bases. We provided four definitions of digital root [5] [6] [7] [8] and proved that all of them are equal [9] [10] [11]. Notable theorems: digital root of the sum of two numbers is equal to the digital root of the sum of their digital roots [12]; digital root of the product of two numbers is equal to the product of their digital roots [13].
• State transition system: [14] A utility for reasoning about states and transitions. This turned out to be very handy and we use this utility in other formalization projects.
• Knaster-Tarski theorem: [15].
• Real analysis: [16] Inpsired by the real analysis formalization course, we formalized real analysis, but in a slightly different way than presented in the course. Notable theorems include: Bolzano-Weierstrass theorem [17]; completeness of the reals [18]; coherence of the reals [19]; Riemann rearrangement theorem (conditional convergence theorem) [20]. We also implemented a meta program based on typeclass resolution for proving convergence of rational functions [21].
• Cornucopia: [22] Formalization of the Cornucopia esolang.

Active projects

• Angel problem: [23] Formal verification of the solution to the Angel problem. This is a long-term formalization project. Progress can be tracked at User:Hakerh400/Formalization/Angel problem.
• Kolakoski sequence: [24] Verify all facts about the wikipedia:Kolakoski sequence from OEIS. Provide several implementations and prove thay are all equal.
• Trie: [25] Efficient implementation and formal verification of the wikipedia:Trie data structure.
• Lazy list: Formalization of the potentially infinite list data structure.
• Serialization: [26] [27] [28] Implementation of a very fast and formally verified bit-level serialization and deserialization library.
• Axiom or theorem: Formalization of the not-yet-published esolang Axiom or theorem. We will publish the esolang once we formally verify the implementation.
• Sokoban: movable box conjecture: [29] Verification of a partial proof related to the conjecture about a sokoban map. We are formalizing the proof that there is no sokoban map with one box that satisfies the conditions.
• Rectangle with rational side length: [30] Formalize the proof from User:Hakerh400/Rectangle with rational side length. This is currently low priority, because we highly suspect that the proof is incorrect. The theorem itself is correct though.
• Starting digits: Prove that there exists a power of two whose decimal digits start with arbitrary prefix. We are actually formalizing a more general theorem that works for any number base and any exponent base, as long as some conditions are satisfied.

Planned projects

• Computational classes: A library for reasoning about computational classes of esolangs. The Lean library has definitions about Turing machines and languages, but those can't be easily used to prove that a specific esolang is Turing-complete. We plan to develop a library that provides enough utility tools so that we can efficiently prove and formally verify Turing-completeness of many esolangs.
• Emanator: Implement a formally verified interpreter for Emanator and prove that the Kolakoski sequence generator program is correct.
• But Is It Art?: Implement a formally verified interpreter for But Is It Art? and prove the conjecture about the program that is supposed to accept exactly the strings of As (as nybbles: eb) whose length is a composite number.
• Relations: Implement a formally verified interpreter for Relations.
• Recurrence equations: Develop a library for reasoning about Recurrence equations.
• Formally verified interactive state-transition systems
• Formally verified I/O
• Dynamic epistemic modal logic with many-world semantics, hierarchical knowledge representation and semi-public announcements: Our goal is to formalize the wikipedia:Cheryl's Birthday problem. There are formalizations of the problem by other scientists, but we are not satisfied with their approaches. We want to do it the right way. So we need to develop a theory for reasoning about dynamic epistemic modal logic.