The readings shared in Mastodon on August 27, 2024 are

• Readings shared August 26, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Prolog #LogicProgramming
• Topological groups (in Isabelle/HOL). ~ Niklas Krofta. #ITP #IsabelleHOL #Math
• Difference bound matrices (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 26, 2024 are

• Proofs that the mirror function of binary trees is involutive in Lean4 and Isabelle/HOL. ~ José A. Alonso (@Jose_AAlonso@mathstodon.xyz). #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalized programming language with speculative execution. ~ Jamie Wright & Andrei Popescu. #ITP #IsabelleHOL
• Game programming in Prolog (Part 1). ~ Youngjin Kang. #Prolog #LogicProgramming

The readings shared in Mastodon on August 24, 2024 are

• Readings shared August 23, 2024. #ITP #IsabelleHOL #LeanProver #Lean4 #AI #DeepLearning #Haskell #FunctionalProgramming #LogicProgramming #Python
• Logic and computation intertwined. ~ Prabhakar Ragde. #Logic #Racket #ITP #Coq #Agda
• Tipos dependientes: λP. ~ Juan Pablo Yamamoto Zazueta. #TypeTheory #CurryHoward

The readings shared in Mastodon on August 23, 2024 are

• Readings shared August 22, 2024. #ITP #Agda #HoTT #Haskell #FunctionalProgramming
• Lean: First steps (06 - Intermediate results). ~ Tariq Rashid (@rzeta0@mastodon.social). #ITP #Lean4 #Math
• How to make mathematicians into programmers (and vice versa). ~ Will Crichton. #ITP #LeanProver #Math
• Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. ~ Lawrence C Paulson (@LawrPaulson@mathstodon.xyz). #ITP #HOL
• Coproduct measure (in Isabelle/HOL). ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang & Xujie Si. #AI #DeepLearning #ITP
• Property-based testing for the people. ~ Harrison Goldstein. #PhDThesis #Haskell #FunctionalProgramming
• Boolean matrix logic programming. ~ Lun Ai & Stephen H. Muggleton. #LogicProgramming
• Ordinals aren't much worse than Quaternions. ~ Philip Zucker (@sandmouth@types.pl). #Python #Math

The readings shared in Mastodon on August 22, 2024 are

• Readings shared August 21, 2024. #ITP #IsabelleHOL #Lean4 #Math #FunctionalProgramming
• Terminal coalgebras and non-wellfounded sets in Homotopy Type Theory. ~ Håkon Robbestad Gylterud, Elisabeth Stenholm & Niccolò Veltri. #ITP #Agda #HoTT
• Prettier. Happier. More Imperative. (Understanding "A prettier printer" by porting it). ~ Benjamin Hodgson. #Haskell #FunctionalProgramming

The readings shared in Mastodon on August 21, 2024 are

• Readings shared August 20, 2024. #ITP #Lean4 #Coq #ACL2 #AlphaProof #Math #Haskell #FunctionalProgramming #Logic #Math #CategoryTheory #TypeTheory
• Probabilistic reasoning and formal proof. ~ Lawrence Paulson (@LawrPaulson@mathstodon.xyz). #ITP #IsabelleHOL #Math
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto (@adolfoneto@bertha.social). #Lean4 #FunctionalProgramming
• Worklist algorithms (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL
• Trustworthy verification of realtime systems. ~ Simon Wimmer. #ITP #IsabelleHOL
• Verified model checking of timed automata. ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 20, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Calculemus
• Improving on AlphaProof: IMO 2024 problem 2 in Lean 4. ~ David Renshaw. #ITP #Lean4 #Math #AlphaProof
• Verification and attack synthesis for network protocols. ~ Max von Hippel. #ITP #ACL2
• A two-phase infinite/finite low-level memory model (Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction). ~ Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski & Steve Zdancewic. #ITP #Coq
• Snapshoble stores. ~ Clément Allain, Basile Clément, Alexandre Moine & Gabriel Scherer. #ITP #Coq
• Refinement composition logic. ~ Youngju Song & Dongjae Lee. #ITP #Coq
• Beyond trees: Calculating graph-based compilers (Functional pearl). ~ Patrick Bahr & Graham Hutton. #Haskell #FunctionalProgramming
• An introduction to categorical proof theory. ~ Amirhossein Akbar Tabatabai. #Logic #Math #CategoryTheory #TypeTheory

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #FunctionalProgramming #Math #Prolog #LogicProgramming
• Proofs of the equivalence of reverse definitions in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalisation of the Mathieu-24 group. ~ Edward van de Meent. #ITP #LeanProver #Lean4 #Math

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 17, 2024. #ITP #LeanProver #Lean4 #Math #AI
• How the Lean language brings math to coding and coding to math. ~ Leo de Moura. #ITP #LeanProver #Math
• Lean again. ~ Adolfo Neto (@adolfoneto@bertha.social). #ITP #Lean4 #FunctionalProgramming
• The semantics of metapropramming in Prolog. ~ David S. Warren. #Prolog #LogicProgramming

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 15, 2024. #ITP #IsabelleHOL #Coq #SSReflect #Math #Haskell #Elm #FunctionalProgramming
• Machine-checked proofs and the rise of formal methods in mathematics. ~ Leonardo de Moura. #ITP #LeanProver #Math
• DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. ~ Huajian Xin et als. #ITP #Lean4
• The AI scientist: Towards fully automated open-ended scientific discovery. ~ Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune & David Ha. #AI