The readings shared in Mastodon on September 12, 2024 are

• Readings shared September 11, 2024. #ITP #IsabelleHOL #LeanProver #Coq #NaprocheZF #Natty #AlphaGeometry #AlphaProof #FunctionalProgramming #OCaml #Logic #Math #IMO #AI #MachineLearning #LLMs
• Proofs of "If p > -1, then (1+p)ⁿ ≥ 1+np" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• The undecidability of contextual equivalence on PCF2 (Towards a mechanisation in Coq). ~ Fabian Andreas Brenner. #ITP #Coq
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov & Anton Podkopaev. #ITP #Coq #LLMs

The readings shared in Mastodon on September 11, 2024 are

• Readings shared September 10, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #Python #Math
• Mathematical Olympiad (To the geometry and beyond…). ~ Mirek Olšák. #Math #ITP #AI #IMO #AlphaGeometry #AlphaProof #LeanProver
• Isabelle/RL project proposal: Reinforcement learning on the Isabelle proof assistant. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL #MachineLearning
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov & Anton Podkopaev. #ITP #Coq #LLMs
• ATPs as universal AIs: What do AGI architectures suggest for ATP research? ~ Zarathustra Goertzel. #ATP #AI
• The formal theory of monads, univalently. ~ Niels van der Weide. #ITP #Coq
• The last mile: How do we make AI theorem provers which work in the real world for real users and not just on benchmarks? ~ Jason Rute. #ITP #AI #LLMs
• Naproche-ZF: Lessons learned from implementing a new natural-language-oriented theorem prover. ~ Adrian De Lon. #ITP #NaprocheZF #Math
• Natural-language proof assistant for higher-order logic. ~ Adam Dingle. #ITP #Natty #Math
• Natty: a natural-language proof assistant with an embedded automatic prover for higher-order logic. ~ Adam Dingle. #ITP #Natty #Math #OCaml
• A few open problems in neural theorem proving (in Lean). ~ Sean Welleck. #ITP #LeanProver #LLMs
• Project description: Experiments with language models for Isabelle autoformalization. ~ David Valente, Manuel Eberl, Cezary Kaliszyk & Josef Urban. #ITP #IsabelleHOL #Autoformalization
• Provably safe systems: Prospects and approaches. ~ Mario Carneiro. #ITP #AI
• With fifth busy beaver, researchers approach computation’s limits. ~ Ben Brubaker. #ITP #Coq #Math #CompSci
• Kids should be taught to think logically. ~ Vinay K. Chaudhri. #Logic

The readings shared in Mastodon on September 10, 2024 are

• Readings shared September 9, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Prolog #LogicProgramming #Python
• Proofs of 0³+1³+2³+3³+···+n³ = (n(n+1)/2)² in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• #Exercitium: Sumas de dos abundantes. #Haskell #Python #Matemáticas
• Types as interfaces. ~ Chris. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 9, 2024 are

• Readings shared September 8, 2024. #ITP #Agda #Math #Haskell #FunctionalProgramming
• Proofs of "a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Describing a knight's tour with Prolog. ~ Markus Triska (@MarkusTriska). #Prolog #FunctionalProgramming
• String Knuth Bendix. ~ Philip Zucker (@sandmouth@types.pl). #Math #Python

The readings shared in Mastodon on September 8, 2024 are

• Readings shared September 7, 2024. #ITP #Lean4 #IsabelleHOL #Maude #ATP #Prover9 #Math #Calculemus
• Formalization of the structure sheaf of a ring spectrum. ~ Maša Žaucer. #ITP #Agda #Math
• Automatic test-case generation for Haskell based on dependent types. ~ Pablo Castellanos García. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 7, 2024 are

• Readings shared September 6, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #PVS #Logic #HOL4 #Lisa #Mizar #ACL2 #Math #AI #MachineLearning
• Proofs of "a+(a+d)+(a+2d)+···+(a+nd) = (n+1)(2a+nd)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Metaprogramming in Lean. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Examples using MetaProgramming for writing tactics. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Formalisation of Hall’s theorem for countable infinite graphs. ~ Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón & Thaynara Arielly de Lima. #ITP #IsabelleHOL #Math
• First-order theorem proving with power maps in semigroups. ~ Yi Lin1, Ranganathan Padmanabhan & Yang Zhang. #ATP #Prover9 #Math
• Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. #ITP #Maude #LeanProver #Lean3

The readings shared in Mastodon on September 6, 2024 are

• Readings shared September 5, 2024. #ITP #LeanProver #Lean4 #IsabelleHO #Agda #Logic #Math #Calculemus #Haskell #OCaml #FunctionalProgramming #AI
• Towards solid abelian groups: A formal proof of Nöbeling’s theorem. ~ Dagur Asgeirsson. #ITP #LeanProver #Math
• The directed Van Kampen theorem in Lean. ~ Henning Basold, Peter Bruin & Dominique Lawson. #ITP #LeanProver #Lean4 #Math
• Verifying peephole rewriting in SSA compiler IRs. ~ Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens & Tobias Grosser. #ITP #LeanProver
• Duper: A proof-producing superposition theorem prover for dependent type theory. ~ Joshua Clune, Yicheng Qian, Alexander Bentkamp & Jeremy Avigad. #ITP #LeanProver #Lean4
• Teaching mathematics using Lean and controlled natural language. ~ Patrick Massot. #ITP #LeanProver #Lean4 #Math
• Lean formalization of completeness proof for Coalition Logic with Common Knowledge. ~ Kai Obendrauf, Anne Baanen, Patrick Koopmann & Vera Stebletsova. #ITP #LeanProver #Lean4
• Formal verification of the empty hexagon number. ~ Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro & Marijn J. H. Heule. #ITP #LeanProver #Lean4
• Integrals within integrals: A formalization of the Gagliardo-Nirenberg-Sobolev inequality. ~ Floris van Doorn & Heather Macbeth. #ITP #LeanProver #Lean4 #Math
• Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4. ~ Sam Ezeh. #ITP #LeanProver #Lean4 #Math
• Formalising half of a graduate textbook on number theory. ~ Manuel Eberl, Anthony Bordg, Lawrence C. Paulson & Wenda Li. #ITP #IsabelleHOL #Math
• A formalization of the Lévy-Prokhorov metric in Isabelle/HOL. ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• Alpha-beta pruning verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
• A formal analysis of capacity scaling algorithms for minimum cost flows. ~ Mohammad Abdulaziz & Thomas Ammer. #ITP #IsabelleHOL
• An operational semantics in Isabelle/HOL-CSP. ~ Benoît Ballenghien & Burkhart Wolff. #ITP #IsabelleHOL
• A verified earley parser. ~ Martin Rau & Tobias Nipkow. #ITP #IsabelleHOL
• A modular formalization of superposition in Isabelle/HOL. ~ Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette & Sophie Tourret. #ITP #IsabelleHOL
• Distributed parallel build for the Isabelle Archive of Formal Proofs. ~ Fabian Huch & Makarius Wenzel. #ITP #IsabelleHOL
• A generalised union of rely–guarantee and separation logic using permission algebras. ~ Vincent Jackson, Toby Murray & Christine Rizkallah. #ITP #IsabelleHOL
• An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility. ~ Dohan Kim. #ITP #IsabelleHOL
• A Coq formalization of Taylor models and power series for solving ordinary differential equations. ~ Sewon Park & Holger Thies. #ITP #Coq #Math
• A comprehensive overview of the Lebesgue differentiation theorem in Coq. ~ Reynald Affeldt & Zachary Stone. #ITP #Coq #Math
• Taming differentiable logics with Coq formalisation. ~ Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz & Kathrin Stark. #ITP #Coq #Logic #MachineLearning
• Completeness of asynchronous session tree subtyping in Coq. ~ Burak Ekici & Nobuko Yoshida. #ITP #Coq
• End-to-end formal verification of a fast and accurate floating-point approximation. ~ Florian Faissole, Paul Geneau de Lamarlière & Guillaume Melquiond. #ITP #Coq
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue & Takafumi Saikawa. #ITP #Coq
• Verifying software emulation of an unsupported hardware instruction. ~ Samuel Gruetter, Thomas Bourgeat & Adam Chlipala. #ITP #Coq
• Modular verification of intrusive list and tree data structures in separation logic. ~ Marc Hermes & Robbert Krebbers. #ITP #Coq
• Formalizing the algebraic small object argument in UniMath. ~ Dennis Hilhorst & Paige Randall North. #ITP #Coq #Math
• The Rewster: Type preserving rewrite rules for the Coq proof assistant. ~ Yann Leray, Gaëtan Gilbert, Nicolas Tabareau & Théo Winterhalter. #ITP #Coq
• Correctly compiling proofs about programs without proving compilers correct. ~ Audrey Seo, Christopher Lam, Dan Grossman & Talia Ringer. #ITP #Coq
• Redex2Coq: Towards a theory of decidability of redex’s reduction semantics. ~ Mallku Soldevila, Rodrigo Ribeiro & Beta Ziliani. #ITP #Coq
• Defining and preserving more C behaviors: Verified compilation using a concrete memory model. ~ Andrew Tolmach, Chris Chhak & Sean Anderson. #ITP #Coq
• Robust mean estimation by all means. ~ Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa & Carsten Schürmann. #ITP #Coq
• Abstractions for multi-sorted substitutions. ~ Hannes Saffrich. #ITP #Agda
• The functor of points approach to schemes in Cubical Agda. ~ Max Zeuner & Matthias Hutzler. #ITP #Agda
• A formalization of the general theory of quaternions. ~ Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro & Mauricio Ayala-Rincón. #ITP #PVS #Math
• Formalizing the Cholesky factorization theorem. ~ Carl Kwan & Warren A. Hunt Jr. #ITP #ACL2 #Math
• A formal proof of R(4,5)=25. ~ Thibault Gauthier & Chad E. Brown. #ITP #HOL4 #Math
• Mechanized HOL reasoning in set theory. ~ Simon Guilloud, Sankalp Gambhir, Andrea Gilot & Viktor Kunčak. #ITP #Lisa #Math
• Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. ~ Karol Pąk & Cezary Kaliszyk. #ITP #Mizar #Math
• 15th International Conference on Interactive Theorem Proving (ITP 2024,). #ITP
• The code of Mathematics: Proof and truth ~ Stefan Müller-Stach. #Math
• Neuro-symbolic theorem proving with Lean. ~ Peiyang Song (@p_song1). #ITP #LeanProver #AI #MachineLearning

The readings shared in Mastodon on September 5, 2024 are

• Readings shared September 4, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #FunctionalProgramming
• Proofs of "0+1+2+3+···+n=n(n + 1)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Lean: First steps (07 - Proof by cases). ~ Tariq Rashid (@rzeta0@mastodon.social). #ITP #Lean4 #Math
• Logic and proof. ~ Jeremy Avigad, Robert Y. Lewis & Floris van Doorn. #ITP #LeanProver #Lean4 #Logic #Math
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch & Axel Ljungström.3# #ITP #Agda
• Sized types and coinduction in Safe Agda. ~ Isaac Elliott. #Agda #FunctionalProgramming
• OCaml scientific computing. #OCaml #FunctionalProgramming #AI
• LSP: the good, the bad, and the ugly. ~ Michael Peyton Jones (@mpeytonjones). #Haskell #FunctionalProgramming
• Parsers are relative bimonads. ~ Artemis. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 4, 2024 are

• Readings shared September 3, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Proofs of "If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Seven levels of type safety in Haskell: Lists. ~ Justin Lê (@mstk). #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 3, 2024 are

• Readings shared September 2, 2024. #ITP #Lean4 #LeanProver #IsabelleHOL #Coq #Maude #Math #Calculemus #FunctionalProgramming
• Proofs of "If x is the limit of u and y is an upper bound of u, then x ≤ y" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• An exponential improvement for diagonal Ramsey (in Isabelle/HOL). ~ Lawrence C. Paulson (@LawrPaulson@mathstodon.xyz). #ITP #IsabelleHOL #Math
• Extension of stateful intransitive noninterference with inputs, outputs, and nondeterminism in language IMP. ~ Pasquale Noce. #ITP #IsabelleHOL
• Definitive set semantics for LTL3 (in Isabelle/HOL). ~ Rayhana Amjad, Rob van Glabbeek & Liam O’Connor. #ITP #IsabelleHOL