The readings shared in Bluesky on 9 July 2025 are

• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• Doing Lean dirty: Lean as a Jupyter notebook replacement. ~ Philip Zucker. #ITP #LeanProver
• Robust, end-to-end correctness proofs of industrial divide and square root RTL designs. ~ Sol Swords, Cuong Chau. #ITP #ACL2
• The φ-weighted recognition hamiltonian: A self-adjoint operator unifying automorphic L-functions, E 8 symmetry, and cosmic dynamics. #ITP #LeanProver
• Computational p-adics (in Isabelle/HOL). ~ Jeremy Sylvestre. #ITP #IsabelleHOL #Math
• The oneway to hiding theorem (in Isabelle/HOL). ~ Katharina Kreuzer, Dominique Unruh. #ITP #IsabelleHOL
• Kraus maps (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL
• Parikh's theorem (in Isabelle/HOL). ~ Fabian Lehr. #ITP #IsabelleHOL
• Computer-assisted proofs for differential equations and dynamical systems. ~ Maxime Breden. #ITP #Math
• Comparing codes: Binary search in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Verified certificates via SAT and computer algebra systems for the Ramsey R(3,8) and R(3,9) problems. ~ Zhengyu Li et als. #SAT #CAS
• Bourbaki: Self-generated and goal-conditioned MDPs for theorem proving. ~ Matthieu Zimmer et als. #LLMs #ITP #LeanProver
• Clarifying before reasoning: A Coq prover with structural context. ~ Yanzhen Lu et als. #LLMs #ITP #CoqProver
• Curso "Lógica matemática y fundamentos (2019-20)". #Lógica #ProgramaciónFuncional #IsabelleHOL