All pull requests

Pull requests

• refactor: Remove redundant lemmas

  AI-assistedarithmeticprovability logicrefactorset theory
  #1055·SnO2WMaN opened Oct 25, 2026Member·

  ·

• ci: Replace Forgive with lake check

  AI-assistedinfrastructure
  #1052·SnO2WMaN opened Oct 17, 2026Member·

  ·

• doc: No proof strategy in docstrings

  AI-assisteddocumentation
  #1049·SnO2WMaN opened Oct 10, 2026Member·

  ·

• add(FirstOrder): liberalize bounded functions

  #1046·iehality opened Oct 9, 2026Member·

  ·

• add(FirstOrder/Arithmetic): Parikh's theorem

  AI-assistedAlpha-Centauriarithmetic
  #1045·SnO2WMaN opened Oct 9, 2026Member·

  ·

• add(FirstOrder/Arithmetic): Basic model theoretical setup

  AI-assistedAlpha-Centauriarithmetic
  #1043·SnO2WMaN opened Oct 9, 2026Member·

  ·
  3

• add(FirstOrder/Arithmetic): @[primrec] for Δ₀ truth and term evaluation

  AI-assistedAlpha-Centauriarithmetic
  #1042·SnO2WMaN opened Oct 9, 2026Member·

  ·

• add(FirstOrder/Arithmetic): Primitive recursive functions are 𝗜𝚺₁-provably total

  AI-assistedAlpha-Centauriarithmetic
  #1041·SnO2WMaN opened Oct 9, 2026Member·

  ·
  9

• add(Arithmetic): finite axiomatizability of 𝗜𝚺 n

  AI-assistedAlpha-Centauriarithmetic
  #1019·SnO2WMaN opened Sep 29, 2026Member·

  ·
  1

• docs: add formalization.yaml

  AI-assisteddocumentation
  #1017·SnO2WMaN opened Sep 28, 2026Member·

  ·
  1

• refactor(FirstOrder): parameterize the bounded hierarchy by an initial class

  AI-assistedarithmeticrefactor
  #1016·SnO2WMaN opened Sep 28, 2026Member·

  ·

• add(FirstOrder/Concat): Language of Theory of Concatenation

  #808·SnO2WMaN opened Mar 9, 2026Member·

  ·

• add(SetTheory): Recursion, ordinal addition and multiplication

  set theory
  #799·tosiaki opened Mar 1, 2026·

  ·
  37

• add(FirstOrder/SetTheory): continuum hypothesis

  set theory
  #647·iehality opened Nov 18, 2025Member·

  ·

• add(FirstOrder): Computable Complete Expansion

  #507·SnO2WMaN opened Aug 9, 2025Member·

  ·