New Foundations is consistent – a difficult mathematical proof proved using Lean

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
  • LeanCopilot

    LLMs as Copilots for Theorem Proving in Lean

  • Then it's time to update your LLM reading!

    https://leandojo.org/

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo
  • con-nf

    A formal consistency proof of Quine's set theory New Foundations

  • But like, you can look at what parts of Mathlib this development imports, it's mainly stuff imported by files in this subdirectory https://github.com/leanprover-community/con-nf/tree/main/Con... , and it's pretty basic things: the definition of a permutation, a cardinal number etc. Almost all of these are things that would feature in the first one or two years of an undergraduate math degree (from just quickly scanning it, the most advanced thing I could see is the definition of cofinality of ordinals). It seems practically impossible to me that someone would make a mistake when e.g. defining what a group is, in a way subtle enough to later break this advanced theorem. If you think that people could mess up that, then all of math would be in doubt.

  • set.mm

    Metamath source file for logic and set theory

  • Correct. The good news that Elements still works otherwise, you just need to add the missing axiom.

    But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list just a few of the many examples of proofs that weren't.

    Sure, there can be bugs in programs, but there are ways to counter such bugs that give FAR more confidence than can be afforded to humans. Lean's approach is to have a small kernel, and then review the kernel. Metamath is even more serious; the Metamath approach is to have an extremely small language, and then re-implement it many times (so that a bug is unlikely to be reproduced in all implementations). The most popular Metamath database is "set.mm", which uses classical logical logic and ZFC. Every change is verified by 5 different verifiers in 5 different programming languages originally developed by 5 different people:

    * metamath.exe aka Cmetamath (the original C verifier by Norman Megill)

    * checkmm (a C++ verifier by Eric Schmidt)

    * smetamath-rs (smm3) (a Rust verifier by Stefan O'Rear)

    * mmj2 (a Java verifier by Mel L. O'Cat and Mario Carneiro)

    * mmverify.py (a Python verifier by Raph Levien)

    For more on these verifiers, see: https://github.com/metamath/set.mm/blob/develop/verifiers.md

  • lean4checker

    Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.

  • Note also that there is an independent checker https://github.com/leanprover/lean4checker to ensure that you're not pulling any fancy tricks at the code level: that the compiled output, free of tactics, is in fact a proof.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts

  • LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

    1 project | /r/math | 11 Dec 2023
  • LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

    1 project | /r/math | 11 Dec 2023
  • AI Will Become Mathematicians' 'Co-Pilot'

    5 projects | news.ycombinator.com | 12 Jun 2024
  • The Fermat's Last Theorem Project

    2 projects | news.ycombinator.com | 1 May 2024
  • Dafny is a verification-aware programming language

    4 projects | news.ycombinator.com | 23 Apr 2024