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