The readings shared in Mastodon on September 16, 2024 are

• Readings shared September 15, 2024. #ITP #LeanProver #Lean4 #LLMs
• Duality theory in linear optimization and its extensions (formally verified). ~ Martin Dvorak & Vladimir Kolmogorov. #ITP #LeanProver #Lean4 #Math
• The Haskell playground. ~ Tom Smeding. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 15, 2024 are

• Readings shared September 14, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Agda #HOL_Light #Math #Haskell #FunctionalProgramming #LambdaCalculus #LLMs
• LLMlean integrates LLMs and Lean for tactic suggestions, proof completion, and more. ~ Sean Welleck et als. #ITP #LeanProver #Lean4 #LLMs
• LeanDojo: Theorem Proving in Lean using Language Models. ~ Kaiyu Yang et als. #ITP #LeanProver #Lean4 #LLMs
• llmstep: [L]LM proofstep suggestions in Lean 4. ~ Sean Welleck et als. #ITP #LeanProver #Lean4 #LLMs

The readings shared in Mastodon on September 14, 2024 are

• Readings shared September 13, 2024. #Haskell #FunctionalProgramming #LiquidHaskell #Emacs #OrgMode
• AI for Mathematics: Mathematical formalized problem solving and theorem proving in different fields in Lean 4. ~ Xichen Tang. #ITP #LeanProver #Lean4 #Math
• Better-performing “25519” elliptic-curve cryptography (Automated reasoning and optimizations specific to CPU microarchitectures improve both performance and assurance of correct implementation). ~ Torben Hansen, John Harrison. #ITP #HOL_Light
• A simple proof that π is irrational (in Isabelle/HOL). ~ Manuel Eberl (@pruvisto@graz.social). #ITP #IsabelleHOL #Math
• Decidable equality for indexed data types. ~ Brent Yorgey (@byorgey@mathstodon.xyz). #ITP #Agda #FunctionalProgramming
• Why Haskell? ~ Gideon Farrell (@gideonfarrell). #Haskell #FunctionalProgramming
• Type-theoretic considerations in functional language software development. ~ David Michael Roberts (@highergeometer@mathstodon.xyz). #Haskell #FunctionalProgramming #ITP #IsabelleHOL
• Simulation of lambda terms in lambda calculus. ~ Helmut Brandl. #LambdaCalculus
• Estrenando el nuevo modelo de OpenAI: o1-preview. Resolviendo con ChatGPT un problema de Matemáticas II de la Prueba de Acceso a la Universidad EBAU. ~ Luis M. Iglesias (@luismiglesias). #LLMs #Matemáticas

The readings shared in Mastodon on September 13, 2024 are

• Readings shared September 12, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #LLMs
• Reflecting away from definitions in Liquid Haskell. ~ Jonathan Arnoult. #Haskell #FunctionalProgramming #LiquidHaskell
• Why and how I use "Org Mode" for my writing and more. ~ Aditya Athalye. #Emacs #OrgMode

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