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