The readings shared in Mastodon on 20 November 2024 are

• Readings shared November 19, 2024. #ITP #Lean4 #Math #Haskell #FunctionalProgramming
• Anatomy of a formal proof. ~ Jeremy Avigad, Johan Commelin, Heather Macbeth, Adam Topaz. #ITP #Lean4 #Math
• A course of Algebra (Part I). ~ Aleksandr Aleksandrovich Zykov. #Math
• El aprendizaje automático ayuda a atacar problemas matemáticos clásicos. ~ Juanjo Rué y Ágata A. Timón. #AI #Math

The readings shared in Mastodon on 19 November 2024 are

• Readings shared November 18, 2024. #LLMs #Math #Reasoning #Logic #TypeTheory
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #Lean4 #Math
• Competitive programming in Haskell: Union-Find, part II. ~ Brent Yorgey (@byorgey@mathstodon.xyz). #Haskell #FunctionalProgramming

The readings shared in Mastodon on 18 November 2024 are

• Readings shared November 17, 2024. #ITP #Coq #Haskell #CommonLisp #FunctionalProgramming #Python #Programming #CategoryTheory
• Do Large Language Models truly grasp mathematics? An empirical exploration from cognitive psychology. ~ Wei Xie, Shuoyoucheng Ma, Zhenhua Wang, Enze Wang, Kai Chen, Xiaobing Sun, Baosheng Wang. #LLMs #Math #Reasoning
• Monoid theory in Alonzo: A little theories formalization in simple type theory. ~ William M. Farmer, Dennis Y. Zvigelsky. #Logic #Math #TypeTheory

The readings shared in Mastodon on 17 November 2024 are

• Readings shared November 16, 2024. #ITP #Lean4 #FunctionalProgramming #Math #AI #LLMs #Git #GitHub
• Designing proof deautomation for Coq. ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Andrew Head, Benjamin C. Pierce. #ITP #Coq
• Type-checking and type-inference. ~ René Thiemann. #Haskell #FunctionalProgramming
• Type-inference in Haskell, kinds and explicit foralls. ~ René Thiemann. #Haskell #FunctionalProgramming
• Functors, record syntax, case study: a simple parser. ~ René Thiemann. #Haskell #FunctionalProgramming
• Monads in general, state monads. ~ René Thiemann. #Haskell #FunctionalProgramming
• Evaluation of monadic code, example: Tseitin, error monads. ~ René Thiemann. #Haskell #FunctionalProgramming
• Parsing in general, Parsec. ~ René Thiemann. #Haskell #FunctionalProgramming
• Number of isomorphism classes of ternary trees. ~ Atabey Kaygun (@atabeykaygun.bsky.social). #FunctionalProgramming #CommonLisp
• Sieves and sheaves. ~ Bartosz Milewski (@bartoszmilewski.bsky.social). #CategoryTheory
• Python is no more the king of data science (5 reasons why Python is losing its crown). ~ Abdur Rahman. #Python #Programming

The readings shared in Mastodon on 16 November 2024 are

• Readings shared November 15, 2024. #ITP #LeanProver #Math #SetTheory #Haskell #FunctionalProgramming #AI #LLMs
• Code with proofs: The Arena. #ITP #Lean4 #FunctionalProgramming
• The Turing Test and our shifting conceptions of intelligence. ~ Melanie Mitchell (@melaniemitchell.bsky.social). #AI
• Debates on the nature of artificial general intelligence. ~ Melanie Mitchell (@melaniemitchell.bsky.social). #AI
• Large Language Models. ~ Melanie Mitchell (@melaniemitchell.bsky.social). #AI #LLMs
• GitHub for mathematicians. ~ Steven Clontz. #Git #GitHub
• Code4math: Consortium of Digital Ecosystems for Mathematics. #Math

The readings shared in Mastodon on 15 November 2024 are

• Readings shared November 14, 2024. #ITP #LeanProver #Coq #ATP #Logic #Math #Haskell #FunctionalProgramming #FormalMethods #CompSci #Education #RustLang #AI #LLMs
• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• The Haskell inlining and specialization FAQ. ~ Gabriella Gonzalez (@GabriellaG439). #Haskell #FunctionalProgramming
• Axiomatic set theory (Version of 9 November 2024). ~ Tom Leinster. #Math #SetTheory
• The metaphors of artificial intelligence. ~ Melanie Mitchell. #AI #LLMs

The readings shared in Mastodon on 14 November 2024 are

• Readings shared November 13, 2024. #ITP #Lean4 #Math #Physics #ATP #SAT_Solvers
• VEL: A formally verified reasoner for ℰℒ++ description logic. ~ Atalay Mert Ileri1, Hande Küçük McGinty. #ITP #Coq #Logic
• La formalización automatizada de las matemática: Una historia de cómo la necesidad hizo la virtud. ~ David de Frutos Escrig. #ITP #LeanProver #Math
• Debugging Haskell type errors. ~ Tikhon Jelvis (@tikhonjelvis). #Haskell #FunctionalProgramming
• The role of formal methods in computer science education. ~ Maurice ter Beek, Manfred Broy, Brijesh Dongol. #FormalMethods #CompSci #Education
• Resolution prover in Rust. ~ Wanda Rosmus. #Logic #ATP #RustLang
• AI’s math problem: FrontierMath benchmark shows how far technology still has to go. ~ Michael Nuñez (@MichaelFNunez). #AI #Math
• A holistic and critical look at language agents. ~ Yu Su (@ysu_nlp). #AI #LLMs

The readings shared in Mastodon on 13 November 2024 are

• Readings shared November 12, 2024. #ITP #LeanProver #LLMs #Emacs
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio, Adam Topaz. #ITP #Lean4 #Math
• Formalization of physics index notation in Lean 4. ~ Joseph Tooby-Smith. #ITP #Lean4 #Math #Physics
• How to discover short, shorter, and the shortest proofs of unsatisfiability: A branch-and-bound approach for resolution proof length minimization. ~ Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović. #ATP #SAT_Solvers

The readings shared in Mastodon on 12 November 2024 are

• Readings shared November 11, 2024. #ITP #LeanProver #Logic #Math #LLMs
• Benchmarking automated theorem proving with Large Language Models. ~ Vanessa Lama, Catherine Ma, Tirthankar Ghosal. #ITP #LeanProver #LLMs
• BC-Prover: Backward chaining prover for formal theorem proving. ~ Yuhang He et als. #ITP #LeanProver #LLMs
• Programación literaria en Emacs (1ª parte). ~ Nyan Max (@maxxcan@mastodon.social). #Emacs

The readings shared in Mastodon on 11 November 2024 are

• Readings shared November 10, 2024. #ITP #Lean4 #Logic #Math #TFM
• NL²PS: A natural language to Lean proofs system. ~ Yifan Luo, Kangping Xu.V#discussion #ITP #LeanProver #LLMs
• VCVio: A formally verified forking lemma and Fiat-Shamir transform, via a flexible and expressive oracle representation. ~ Devon Tuma, Nicholas Hopper. #ITP #LeanProver
• The art of proof (Basic training for deeper mathematics). ~ Matthias Beck, Ross Geoghegan. #Logic #Math