Skip to content
Change the repository type filter

All

    Repositories list

    • Lean
      0000Updated May 20, 2024May 20, 2024
    • Lean
      0000Updated Apr 17, 2024Apr 17, 2024
    • BICMR-ai4math 寒假研讨班第3组:algebraic_integers_of_Q_adjoin_sqrt_-3_is_PID
      Lean
      0000Updated Apr 11, 2024Apr 11, 2024
    • 寒假讨论班第五组----九点圆
      Lean
      0000Updated Jan 31, 2024Jan 31, 2024
    • BICMR第一小组五点共圆问题形式化
      Lean
      0100Updated Jan 28, 2024Jan 28, 2024
    • pq阶群非单(p、q为互异素数)
      0000Updated Jan 26, 2024Jan 26, 2024
    • Lean
      0000Updated Jan 26, 2024Jan 26, 2024
    • A formalization project for finite dimensional Lie algebra representation
      Lean
      0000Updated Jan 26, 2024Jan 26, 2024
    • 0100Updated Jan 26, 2024Jan 26, 2024
    • problem 2.13/2.15
      Lean
      0000Updated Jan 26, 2024Jan 26, 2024
    • Group7-3D

      Public
      BICMR-ai4math 寒假研讨班第七组:一二三维 Lie 代数分类 (三维)
      Lean
      Apache License 2.0
      0000Updated Jan 25, 2024Jan 25, 2024
    • BICMR-ai4math 寒假研讨班第七组:一二三维 Lie 代数分类 (一维、二维)
      Lean
      Apache License 2.0
      0000Updated Jan 25, 2024Jan 25, 2024
    • group-9-Number-Theory-P1
      Lean
      0000Updated Jan 25, 2024Jan 25, 2024
    • Lean
      0000Updated Jan 22, 2024Jan 22, 2024
    • TypeScript
      1600Updated Jan 11, 2024Jan 11, 2024
    • Shell
      0100Updated Oct 14, 2023Oct 14, 2023
    • All-in-one mirror utility for SJTUG mirror
      Rust
      Apache License 2.0
      10000Updated Sep 29, 2023Sep 29, 2023
    • elan

      Public
      A Lean version manager
      Rust
      Apache License 2.0
      35000Updated Sep 29, 2023Sep 29, 2023
    • Operad

      Public
      Lean
      0000Updated Sep 23, 2023Sep 23, 2023
    • Lean
      0200Updated Aug 20, 2023Aug 20, 2023
    • sol-2-9

      Public
      The repository contains Lean code that implements problem 2-9
      Lean
      1001Updated Aug 4, 2023Aug 4, 2023
    • sol-2-11

      Public
      Four lemmas
      Lean
      0000Updated Aug 2, 2023Aug 2, 2023
    • sol-2-10

      Public
      0000Updated Aug 2, 2023Aug 2, 2023
    • sol-2-14

      Public
      0000Updated 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
      0000Updated 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
      0000Updated Aug 2, 2023Aug 2, 2023
    • 0000Updated Aug 1, 2023Aug 1, 2023
    • sol-2-19

      Public
      Lean
      3100Updated Jul 31, 2023Jul 31, 2023