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