Data

Tools

Indexes

Applications

Experiments

Open Source Science

flt

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

https://github.com/imperialcollegelondon/flt

Science Score: 44.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (6.0%) to scientific vocabulary
Last synced: 6 months ago · JSON representation ·

Repository

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Basic Info
Statistics
  • Stars: 664
  • Watchers: 17
  • Forks: 94
  • Open Issues: 38
  • Releases: 23
Created over 2 years ago · Last pushed 6 months ago
Metadata Files
Readme Contributing License Code of conduct Citation

README.md

Fermat's Last Theorem

Website Documentation Blueprint Paper Gitpod Ready-to-Code

An ongoing multi-author open source project to formalise a proof of Fermat's Last Theorem in the Lean theorem prover.

Information about the project

The project is currently being led by Kevin Buzzard. Until September 2029 it is being funded by grant EP/Y022904/1, awarded by the EPSRC. The project is hosted at Imperial College London. Kevin would like to extend many many thanks to both of these institutions for their ongoing support of this nonstandard research.

General information ("What is Fermat's Last Theorem/Lean?" / "Why are you doing this?" etc) is here.

The route we will be taking was planned out essentially entirely by Richard Taylor in discussions with Buzzard. It is a modern variant of the original Wiles/Taylor-Wiles proof. For more details about the mathematics behind the proof, a good place to start is the blueprint.

Information on how to contribute is available here.

Owner

  • Name: Imperial College London
  • Login: ImperialCollegeLondon
  • Kind: organization
  • Email: icgithub-support@imperial.ac.uk
  • Location: Imperial College London

Imperial College main code repository

Citation (CITATION.bib) 

@software{FLT_Lean,
         abstract     = {An ongoing Lean formalization of Fermat's Last Theorem.},
         author       = {Buzzard, Kevin and Taylor, Richard},
         institution  = {Imperial College London},
         keywords     = {Fermat's Last Theorem, Fermats Last Theorem, Lean, Lean4, Formal Methods, Formal Verification, Theorem Proving, Interactive Theorem Proving, Proof Assistant, Mathematical Formalization, Formal Mathematics, Blueprint, Type Theory, Computer-Assisted Proof, Mathematical Software, Research Software Engineering},
         license      = {Apache License 2.0},
         title        = {{FLT}},
         year         = {2025}
         }

Issues and Pull Requests

Last synced: 6 months ago

All Time
  • Total issues: 155
  • Total pull requests: 744
  • Average time to close issues: 18 days
  • Average time to close pull requests: 4 days
  • Total issue authors: 6
  • Total pull request authors: 57
  • Average comments per issue: 1.16
  • Average comments per pull request: 1.03
  • Merged pull requests: 572
  • Bot issues: 42
  • Bot pull requests: 67
Past Year
  • Issues: 146
  • Pull requests: 557
  • Average time to close issues: 14 days
  • Average time to close pull requests: 3 days
  • Issue authors: 6
  • Pull request authors: 39
  • Average comments per issue: 1.17
  • Average comments per pull request: 1.01
  • Merged pull requests: 422
  • Bot issues: 42
  • Bot pull requests: 58
View more stats
Top Authors
Issue Authors
  • kbuzzard (100)
  • github-actions[bot] (42)
  • pitmonticone (7)
  • YaelDillies (4)
  • morrison-daniel (1)
  • DavidMichaelRoberts (1)
Pull Request Authors
  • kbuzzard (150)
  • Ruben-VandeVelde (132)
  • pitmonticone (97)
  • github-actions[bot] (39)
  • YaelDillies (35)
  • dependabot[bot] (28)
  • smmercuri (27)
  • matthewjasper (20)
  • javierlcontreras (16)
  • erdOne (12)
  • kim-em (11)
  • WilliamCoram (11)
  • utensil (10)
  • digama0 (9)
  • b-mehta (8)
Top Labels
Issue Labels
auto-update-lean-fail (14) straightforward (5) WIP (2) Big Proof (1)
Pull Request Labels
auto-update-lean (39) dependencies (26) awaiting-CI (25) awaiting-review (22) github_actions (11) WIP (10) awaiting-author (10) ruby (6) awaiting author (3) do-not-merge (2)

Dependencies

docs/Gemfile.lock rubygems
  • 102 dependencies
.github/workflows/push.yml actions
  • actions/cache v3 composite
  • actions/checkout v2 composite
  • actions/deploy-pages v1 composite
  • actions/upload-pages-artifact v1 composite
  • ruby/setup-ruby v1 composite
  • xu-cheng/texlive-action v2 composite
.github/workflows/push_pr.yml actions
  • actions/checkout v2 composite
blueprint/requirements.txt pypi
  • invoke ==2.2.0
  • pandoc ==2.3
  • watchfiles ==0.16.1
docs/Gemfile rubygems
  • github-pages >= 0 development
  • http_parser.rb ~> 0.6.0
  • tzinfo ~> 1.2
  • tzinfo-data >= 0
  • wdm ~> 0.1.1
  • webrick ~> 1.7