Issues

• FreyPackage docstring: 1993 announcement and 1995 proof of modularity

  ImperialCollegeLondon/FLT#1211 · Filter by author SonnyChecksIn opened on Nov 8, 2026

• group_theory_lemma (EllipticCurve/Torsion): proof available via Mathlib PR #45439

  ImperialCollegeLondon/FLT#1209 · Filter by author ejackson-vp opened on Oct 28, 2026

• scripts/pre-push.sh checks for lakefile.lean, so the installed pre-push hook always fails

  ImperialCollegeLondon/FLT#1133 · Filter by author anagnorisis2peripeteia opened on Jul 24, 2026
  2

• forbid any change to FLTTest.lean

  ImperialCollegeLondon/FLT#1116 · Filter by author Whysoserioushah opened on Jul 11, 2026
  1

• Weil pairing

  Logos Workshop
  ImperialCollegeLondon/FLT#1065 · Filter by author kbuzzard opened on Jul 6, 2026
  1

• n-torsion in elliptic curve has size n^2

  Logos Workshop
  ImperialCollegeLondon/FLT#1064 · Filter by author kbuzzard opened on Jul 6, 2026
  1

• Tate uniformisation of ell curve with split mult reduction

  ImperialCollegeLondon/FLT#1063 · Filter by author kbuzzard opened on Jul 6, 2026

• Quadratic twists

  Logos Workshop
  ImperialCollegeLondon/FLT#1062 · Filter by author kbuzzard opened on Jul 6, 2026
  2

• The Tate curve construction

  Logos Workshop
  ImperialCollegeLondon/FLT#1061 · Filter by author kbuzzard opened on Jul 6, 2026

• n-torsion in elliptic curves with good reduction is flat

  Logos Workshop
  ImperialCollegeLondon/FLT#1060 · Filter by author kbuzzard opened on Jul 6, 2026
  1

• slow typeclass inference for infinite place completions

  ImperialCollegeLondon/FLT#891 · Filter by author kbuzzard opened on Apr 15, 2026
  2

• unfolding in typeclass isdefeq check for adicCompletion

  ImperialCollegeLondon/FLT#889 · Filter by author kbuzzard opened on Apr 15, 2026
  2

• Equivalence between QHat/ZHat and FiniteAdeleRing

  ImperialCollegeLondon/FLT#737 · Filter by author bwangpj opened on Oct 3, 2025
  2

• Central simple algebra tensor simple ring is simple ring

  Task

  ImperialCollegeLondon/FLT#631 · Filter by author kbuzzard opened on Jun 12, 2025
  1

  

• The Hecke algebra associated to a level U_1(S) structure is commutative

  Task

  ImperialCollegeLondon/FLT#585 · Filter by author kbuzzard opened on May 31, 2025
  2

  

• Hecke operators U_alpha and U_beta at a bad prime commute

  Task

  ImperialCollegeLondon/FLT#584 · Filter by author kbuzzard opened on May 31, 2025
  1

  

• AutomorphicForm/QuaternionAlgebra/Defs is slow

  ImperialCollegeLondon/FLT#564 · Filter by author kbuzzard opened on May 27, 2025
  5

• Haar character of reals/complexes etc is for the wrong function

  ImperialCollegeLondon/FLT#529 · Filter by author kbuzzard opened on May 20, 2025
  

• Left and right multiplication on a simple algebra have the same determinant

  Task

  ImperialCollegeLondon/FLT#518 · Filter by author kbuzzard opened on May 18, 2025
  1

  

• Pullback of Haar measure along an open embedding

  Task

  ImperialCollegeLondon/FLT#507 · Filter by author kbuzzard opened on May 18, 2025
  2

  

• Mazur's theorem

  assumption
  ImperialCollegeLondon/FLT#477 · Filter by author kbuzzard opened on May 10, 2025

• Odlyzko bounds

  assumption
  ImperialCollegeLondon/FLT#458 · Filter by author kbuzzard opened on Apr 30, 2025
  9

• re-add Frobenius project

  Big Proof
  ImperialCollegeLondon/FLT#447 · Filter by author kbuzzard opened on Apr 29, 2025
  5

• Copyright headers

  ImperialCollegeLondon/FLT#423 · Filter by author kbuzzard opened on Apr 19, 2025
  1

  

• linters I would like

  ImperialCollegeLondon/FLT#418 · Filter by author kbuzzard opened on Apr 16, 2025
  11