Repositories list

• abstract-algebra-template

  Public
  Lean

  •0•0•0•0•Updated May 20, 2024May 20, 2024

• G12_Myerson-s-Lemma

  Public
  Lean

  •0•0•0•0•Updated Apr 17, 2024Apr 17, 2024

• group3-algebraic_integers_of_Q_adjoin_sqrt_-3_is_PID

  Public
  BICMR-ai4math 寒假研讨班第3组:algebraic_integers_of_Q_adjoin_sqrt_-3_is_PID

  Lean

  •0•0•0•0•Updated Apr 11, 2024Apr 11, 2024

• Group5_Nine_Point_Circle

  Public
  寒假讨论班第五组----九点圆

  Lean

  •0•0•0•0•Updated Jan 31, 2024Jan 31, 2024

• Group_1_JZM_problem

  Public
  BICMR第一小组五点共圆问题形式化

  Lean

  •0•1•0•0•Updated Jan 28, 2024Jan 28, 2024

• Group_pq_notSimple-by-lean4

  Public
  pq阶群非单（p、q为互异素数）

  0•0•0•0•Updated Jan 26, 2024Jan 26, 2024

• Group13-CLT

  Public
  Lean

  •0•0•0•0•Updated Jan 26, 2024Jan 26, 2024

• Group6-Formalization-on-Lie-algebra-rep

  Public
  A formalization project for finite dimensional Lie algebra representation

  Lean

  •0•0•0•0•Updated Jan 26, 2024Jan 26, 2024

• Group4_BFGS_update

  Public
  0•1•0•0•Updated Jan 26, 2024Jan 26, 2024

• Group10-2.13-2.15

  Public
  problem 2.13/2.15

  Lean

  •0•0•0•0•Updated Jan 26, 2024Jan 26, 2024

• Group7-3D

  Public
  BICMR-ai4math 寒假研讨班第七组：一二三维 Lie 代数分类 (三维)

  Lean

  •

  Apache License 2.0

  •0•0•0•0•Updated Jan 25, 2024Jan 25, 2024

• Group7-1D-2D

  Public
  BICMR-ai4math 寒假研讨班第七组：一二三维 Lie 代数分类 (一维、二维)

  Lean

  •

  Apache License 2.0

  •0•0•0•0•Updated Jan 25, 2024Jan 25, 2024

• group-9-Number-Theory-P1

  Public
  group-9-Number-Theory-P1

  Lean

  •0•0•0•0•Updated Jan 25, 2024Jan 25, 2024

• group-0-p-0

  Public
  Lean

  •0•0•0•0•Updated Jan 22, 2024Jan 22, 2024

• bicmr-ai4math.github.io

  Public
  https://bicmr-ai4math.github.io

  TypeScript

  •1•6•0•0•Updated Jan 11, 2024Jan 11, 2024

• lean-simple-mirror

  Public
  Shell

  •0•1•0•0•Updated Oct 14, 2023Oct 14, 2023

• mirror-clone

  Public
  All-in-one mirror utility for SJTUG mirror

  Rust

  •

  Apache License 2.0

  •10•0•0•0•Updated Sep 29, 2023Sep 29, 2023

• elan

  Public
  A Lean version manager

  Rust

  •

  Apache License 2.0

  •34•0•0•0•Updated Sep 29, 2023Sep 29, 2023

• Operad

  Public
  Lean

  •0•0•0•0•Updated Sep 23, 2023Sep 23, 2023

• spectral-sequence

  Public
  Lean

  •0•2•0•0•Updated Aug 20, 2023Aug 20, 2023

• sol-2-9

  Public
  The repository contains Lean code that implements problem 2-9

  Lean

  •1•0•0•1•Updated Aug 4, 2023Aug 4, 2023

• sol-2-11

  Public
  Four lemmas

  Lean

  •0•0•0•0•Updated Aug 2, 2023Aug 2, 2023

• sol-2-10

  Public
  0•0•0•0•Updated Aug 2, 2023Aug 2, 2023

• sol-2-14

  Public
  0•0•0•0•Updated Aug 2, 2023Aug 2, 2023

• sol-2-16

  Public
  For positive integers $a, s, t$, prove that $a^{\mathrm{gcd}(s,t)}-1=\mathrm{gcd}(a^s-1,a^t-1)$. As a bonus, it can be proven that for any positive integer $n>1$, $n \nmid 2^n-1$.

  Lean

  •0•0•0•0•Updated Aug 2, 2023Aug 2, 2023

• sol-2-6

  Public
  for two subgroups H1, H2 of a group G such that H1 ∪ H2 is a subgroup, prove that H1, H2 have mutual inclusion relations

  0•0•0•0•Updated Aug 2, 2023Aug 2, 2023

• course-invite

  Public
  0•0•0•0•Updated Aug 1, 2023Aug 1, 2023

• sol-2-19

  Public
  Lean

  •3•1•0•0•Updated Jul 31, 2023Jul 31, 2023