Readings shared June 6, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/06-readings_shared_06-06-25 #FunctionalProgramming #Haskell #ITP #Lean4 #Math
Libro "Matemáticas en Lean4" (versión del 6-junio-25). https://raw.githubusercontent.com/jaalonso/Matematicas_en_Lean4/main/Matematicas_en_Lean4.pdf #ITP #Lean4 #Math
A third video in my occasional series on #Lean4 formalization workflows, this time focusing on how relying extensively on #GitHubCopilot fares against standard "epsilon delta" type problems in analysis. https://www.youtube.com/watch?v=c1ixXMtmfS8
DeepSeek Releases Massive 671B Prover V2 Model For Mathematical Theorem Proving Ahead of R2 Release
#AI #ChinaAI #DeepSeek #OpenSourceAI #Math #TheoremProving #Lean4 #MachineLearning #DeepLearning #MathAI
Readings shared January 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/21-readings_shared_01-21-25 #ITP #Lean4 #IsabelleHOL #Math #Prolog #LogicProgramming #AI #LLMs
Proofs of the Praeclarum Theorema in Lean4 and Isabelle/HOL. https://jaalonso.github.io/calculemus/posts/2025/01/21-praeclarum_theorema/ #ITP #Lean4 #IsabelleHOL #Math #Calculemus
Lean: First steps (22 - Recursion) [Video]. ~ Tariq Rashid. https://youtu.be/McHUB7pyj6I #ITP #LeanProver #Lean4 #Math
Lean: First steps (22 - Recursion). ~ Tariq Rashid. https://leanfirststeps.blogspot.com/2025/01/22-recursion.html #ITP #LeanProver #Lean4 #Math
Readings shared January 6, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/06-readings_shared_01-06-25 #ITP #IsabelleHOL #LeanProver #Lean4 #Agda #Coq #Rocq #HoTT #Math #AI #LLMs
Lean: First steps (21 - Simple induction). ~ Tariq Rashid (@rzeta0). https://youtu.be/E55hdgQTcms #ITP #LeanProver #Lean4 #Math
Readings shared January 3, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/03-readings_shared_01-03-25 #ITP #Lean4 #IsabelleHOL #Coq #Rocq #Math #FunctionalProgramming #OCaml #Haskell #Python #AI #MachineLearning
Proofs of the Nicomachus’s theorem in Lean4 and Isabelle/HOL. https://jaalonso.github.io/calculemus/posts/2025/01/03-nicomachus_theorem/ #ITP #Lean4 #IsabelleHOL #Math #Calculemus
Readings shared January 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/01/01-readings_shared_01-01-25 #ITP #LeanProver #Lean4 #Mizar #Math #Haskell #Python
Lean: First steps (21 - Simple induction). ~ Tariq Rashid (@rzeta0). https://leanfirststeps.blogspot.com/2024/12/21-induction.html #ITP #LeanProver #Lean4 #Math
The #Lean4 A* library that I'm currently extracting from my #AdventOfCode project is now nearly at the state that I can push the first commit, but there is one big question I am pondering:
For Advent of Code it only needed to compute the total Costs. It therefore does not have explicit support for outputting the path.
With the Costs being generic [Add], it should be easy enough for users to add path-computation to their Costs type.
Soo, does the library even need to output the path explicitly?
Readings shared December 25, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/25-readings_shared_12-25-24 #Haskell #Python #Math #ITP #LeanProver #Lean4 #Lisp #Programming
Lean: First steps (20 - Contradictory cases). ~ Tariq Rashid (@rzeta0). https://leanfirststeps.blogspot.com/2024/12/20-contradictory-cases.html #ITP #LeanProver #Lean4 #Math
Readings shared December 16, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/16-readings_shared_12-16-24 #ITP #LeanLang #Lean4 #Logic #SMT #Z3 # #Haskell #FunctionalProgramming #CommonLisp #Programming #AI #Math
Readings shared December 12, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/12-readings_shared_12-12-24 #ITP #LeanLang #Lean4 #Math
