Hacker News with Generative AI: Proof Assistants

F*: A proof oriented general purpose programming language (fstar-lang.org)
F* (pronounced F star) is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming.
Programming Languages, Proof Assistants, Functional Programming
254 points by akkad33 24 days ago | 61 comments
Discharging Lean goals into SMT solvers (github.com/ufmg-smite)
This project is inspired by SMTCoq and aims to provide Lean tactics that discharge goals into SMT solvers. It is under active development and is currently in a beta phase. While it is ready for use, it is important to note that there are still some rough edges and ongoing improvements being made.
Software, Proof Assistants, Formal Verification
52 points by ndrwnaguib 58 days ago | 3 comments
Knuckledragger, a Semi-Automated Python Proof Assistant (philipzucker.com)
Python, Programming, Software, Automation, Proof Assistants
71 points by philzook 166 days ago | 24 comments
Translation of Rust's core and alloc crates to Coq for formal verification (formal.land)
Formal Verification, Rust, Programming Languages, Software Engineering, Proof Assistants
358 points by p4bl0 248 days ago | 116 comments
The Fermat's Last Theorem Project (leanprover-community.github.io)
Mathematics, Proof Assistants, Open Source
75 points by happa 263 days ago | 41 comments
New Foundations is consistent – a difficult mathematical proof proved using Lean (leanprover-community.github.io)
Mathematics, Formal Verification, Proof Assistants, Lean
340 points by namanyayg 270 days ago | 162 comments