InfinitePrimes

A proof of the infinitude of primes in Lean 4 from first principles (by ykonstant1)

InfinitePrimes reviews and mentions

Posts with mentions or reviews of InfinitePrimes. We have used some of these posts to build our list of alternatives and similar projects.
  • A slightly longer Lean 4 proof tour
    1 project | news.ycombinator.com | 7 Dec 2023
    Touting my own horn a bit, I have a constructive* proof [0] of the infinitude of prime numbers from first principles: there is no dependence on mathlib so I build all the concepts from scratch. I have been thinking about turning it into a literate code document.

    *The only axiom I cannot avoid is propositional extensionality (which is kind of unavoidable in any non-toy proof in Lean).

    [0] https://github.com/ykonstant1/InfinitePrimes

Stats

Basic InfinitePrimes repo stats
1
7
6.1
7 months ago

The primary programming language of InfinitePrimes is Lean.


Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com