Repositories list

• logical_verification_2024

  Public
  The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)

  Lean

  •4•39•0•0•Updated Mar 28, 2024Mar 28, 2024

• mathlib-classes

  Public
  Use and abuse of instance parameters in the Lean mathematical library

  Lean

  •1•1•0•0•Updated Apr 1, 2023Apr 1, 2023

• class-group-and-mordell-equation

  Public
  Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

  Lean

  •0•3•0•0•Updated Dec 13, 2022Dec 13, 2022

• class-number-journal

  Public
  Lean

  •

  Apache License 2.0

  •0•0•0•0•Updated Jun 24, 2022Jun 24, 2022

• cap_set_problem

  Public
  A formalization of Ellenberg and Gijswijt's solution to the cap set problem.

  Lean

  •0•7•0•0•Updated Jul 4, 2021Jul 4, 2021

• class-number

  Public
  A paper on formalizing Dedekind domains and the class number

  Lean

  •0•3•0•0•Updated Jun 28, 2021Jun 28, 2021

• ring_exp

  Public
  A short paper on the `ring_exp` tactic

  TeX

  •0•1•0•0•Updated Jun 30, 2020Jun 30, 2020

• ring_equational_reasoner

  Public
  Tactic to deduce new equations from given ones (using Gröbner-bases) in a ring or more precisely a commutative algebra over a field

  Lean

  •1•0•0•0•Updated Nov 14, 2019Nov 14, 2019

• mersenne-primes

  Public
  A bijection between Mersenne primes and even perfect numbers

  Lean

  •1•0•0•0•Updated Sep 19, 2019Sep 19, 2019

• field

  Public
  a tactic to normalize field expressions

  Lean

  •0•1•0•0•Updated Jul 22, 2019Jul 22, 2019

• coe_tactic

  Public
  Lean

  •0•0•0•0•Updated May 6, 2019May 6, 2019

• lean-forward

  Public
  0•0•0•0•Updated Jul 3, 2018Jul 3, 2018