Las lecturas compartidas en Mastodon el 27 de junio de 2024 son

• Lecturas compartidas el 26 de junio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂". #ITP #Lean4 #IsabelleHOL #Math
• Error bounds for floating points in Isabelle/HOL. ~ Jan Douwe Beekman. #ITP #IsabelleHOL
• Condensed mathematics in Mathlib. ~ Dagur Asgeirsson. #ITP #Lean4 #Math
• Tactics & keyframes: Visualizing Lean 4 proofs in Blender. ~ David Renshaw. #ITP #Lean4
• miniCodeProps: A minimal benchmark for proving code properties. ~ Evan Lohn, Sean Welleck. #ITP #Lean4 #LLMs
• FVEL: Interactive formal verification environment with large language models via theorem proving. ~ Xiaohan Lin et als. #ITP #IsabelleHOL #LLMs
• Proving olympiad algebraic inequalities without human demonstrations. ~ Chenrui Wei, Mengzhou Sun, Wei Wang. #AIPS #AI #ITP #Math