Hacker News with Generative AI: Proof Assistants

A Formal Proof of Complexity Bounds on Diophantine Equations (arxiv.org)
We present a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalization of our own work in number theory.
Mathematics, Formal Verification, Proof Assistants, Number Theory
52 points by badmonster 4 hours ago | 4 comments
A tool to verify estimates, II: a flexible proof assistant (wordpress.com)
In a recent post, I talked about a proof of concept tool to verify estimates automatically.
Software, Tools, Proof Assistants, Estimates, Verification
69 points by jjgreen 14 days ago | 3 comments
Show HN: TypeScript as a proof assistant for intuitionistic propositional logic (github.com)
TypeScript can be used just like a proof assistant (for intuitionistic propositional logic)!
TypeScript, Proof Assistants, Logic, Programming Languages, Computer Science
17 points by xxmarijnw 53 days ago | 3 comments
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 149 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 183 days ago | 3 comments
Knuckledragger, a Semi-Automated Python Proof Assistant (philipzucker.com)
Python, Programming, Software, Automation, Proof Assistants
71 points by philzook 291 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 374 days ago | 116 comments
The Fermat's Last Theorem Project (leanprover-community.github.io)
Mathematics, Proof Assistants, Open Source
75 points by happa 388 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 396 days ago | 162 comments