Mastodawn

Hacker News Dec 14

Lean Theorem Prover Mathlib

https://github.com/leanprover-community/mathlib4

#HackerNews #Lean #Theorem #Prover #Mathlib #mathlib4 #LeanProver #theoremProving #functionalProgramming

Comparing leanprover-community:master...usernamenotavailablepleasechooseanother:sphericalCoord · leanprover-community/mathlib4

The math library of Lean 4. Contribute to leanprover-community/mathlib4 development by creating an account on GitHub.

GitHub

amen zwa, esq.Aug 5, 2025

In 2023, #Amazon AWS poached #LeonardoDeMoura (the designer of Lean theorem #prover and #programming language) from #Microsoft Research. That sure was a coup.

https://www.amazon.science/blog/how-the-lean-language-brings-math-to-coding-and-coding-to-math

How the Lean language brings math to coding and coding to math

Uses of the functional programming language include formal mathematics, software and hardware verification, AI for math and code synthesis, and math and computer science education.

Amazon Science

N-gated Hacker News Apr 30, 2025

GitHub's latest #AI feature, DeepSeek-Prover-V2, promises to write better code with AI, find #vulnerabilities, and even automate workflows—all while you navigate a labyrinthine menu system likely designed by an M.C. Escher imitator 🎨🔍. Meanwhile, coders everywhere are left wondering if the AI can also automate crying into their keyboards at 3 AM 😭⌨️.
https://github.com/deepseek-ai/DeepSeek-Prover-V2 #GitHub #DeepSeek #Prover #automation #coding #3AM #HackerNews #ngated

GitHub - deepseek-ai/DeepSeek-Prover-V2

Contribute to deepseek-ai/DeepSeek-Prover-V2 development by creating an account on GitHub.

GitHub

Hacker News Apr 30, 2025

DeepSeek-Prover-V2

https://github.com/deepseek-ai/DeepSeek-Prover-V2

#HackerNews #DeepSeek #Prover #V2 #AI #Technology #Innovation #GitHub #OpenSource

GitHub - deepseek-ai/DeepSeek-Prover-V2

Contribute to deepseek-ai/DeepSeek-Prover-V2 development by creating an account on GitHub.

GitHub

Shakthi Kannan Dec 27, 2024

Rocq is a trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics and computer science https://rocq-prover.org/ #Formal #Verification #theorem #prover