Public6hJosé A. Alonso @Jose_A_Alonso@mathstodon.xyzReadings shared March 12, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/12-readings_shared_03-12-25 #AI #ATP #Constraints #Haskell #ITP #IsabelleHOL #Jape #LeanProver #Logic #LogicProgramming #Mace #MachineLearning #Math #NLP #Otter #PVS #PrologVestigium · 1dReadings shared February 12, 2025The readings shared in Bluesky on 12 March 2025 are A formal proof of the irrationality of ζ(3) in Lean 4. ~ Junqi Liu, Jujian Zhang, Lihong Zhi. #ITP #LeanProver #Math #Exercitium: La bandera tricol 0
Public1dJosé A. Alonso @Jose_A_Alonso@mathstodon.xyzCurso "Razonamiento automático (2004-05)". https://jaalonso.github.io/cursos/d-ra-04 #ATP #Otter #Mace #Jape #Logic #ITP #PVSjaalonso.github.ioRazonamiento automático (2004-05) 0
Public1dJosé A. Alonso @Jose_A_Alonso@mathstodon.xyzReadings shared March 11, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/11-readings_shared_03-11-25 #AI #ATP #Emacs #FormalVerification #Haskell #ITP #IsabelleHOL #Jape #LLMs #LeanProver #Logic #LogicProgramming #MAS #Mace #Math #Otter #PVS #Prolog #SMLs #SMT #Scala #Z3Vestigium · 2dReadings shared February 11, 2025The readings shared in Bluesky on 11 March 2025 are Extrinsic termination proofs for well-founded recursion in Lean. ~ Joachim Breitner. #ITP #LeanProver Knuth Bendix solver on Z3 AST. ~ Philip Zucke 0
Public1dJosé A. Alonso @Jose_A_Alonso@mathstodon.xyzCurso "Razonamiento automático (2003-04)". https://jaalonso.github.io/cursos/d-ra-03/index.html #ATP #Otter #Mace #ITP #Jape #PVSjaalonso.github.ioRazonamiento automático (2003-04) 0
