Pull requests

• feat(Logic): the description logic ALC as an instance of the modal framework

  #1166·arademaker opened Oct 26, 2026Collaborator·

  ·
  3

• chore: downstream-lean4 adaptations for nightly-2026-10-25

  #1164·downstream-lean4[bot] opened Oct 26, 2026Bot·

  ·

• feat(RelationAlgebra): integral relation algebras

  #1162·chenson2018 opened Oct 25, 2026Collaborator·3/3·

  ·
  

• feat(RelationAlgebra): atom structures

  #1161·chenson2018 opened Oct 25, 2026Collaborator·2/3·

  ·
  

• feat(RelationAlgebra): a few small lemmas, cleanup

  #1160·chenson2018 opened Oct 25, 2026Collaborator·1/3·

  ·
  8

  

• feat(RAM): add typed random-access machines

  #1158·SamuelSchlesinger opened Oct 23, 2026Collaborator·

  ·
  7

• fix(Transducer): disambiguate translation notation from list indexing

  #1157·SamuelSchlesinger opened Oct 23, 2026Collaborator·

  ·

• feat(Logic): semantic consequence, with Kleene K3 as an instance

  #1156·jessealama opened Oct 22, 2026Contributor·1 task·

  ·

• feat(MultiTapeTM): loglogn_equals_no_space

  #1154·barni120400 opened Oct 19, 2026Contributor·

  ·

• refactor(MultiTapeTM): share computation predicates

  #1153·barni120400 opened Oct 19, 2026Contributor·

  ·

• feat(MultiTapeTM): input shortening

  #1152·barni120400 opened Oct 19, 2026Contributor·

  ·

• refactor(MultiTape): simulate machines through adapters

  #1151·barni120400 opened Oct 19, 2026Contributor·

  ·

• feat(List): extendable prefixes of right-maximal repeats

  #1149·iosephusferrum opened Oct 19, 2026Contributor·

  ·

• feat(Automata): Thompson's construction

  #1148·iosephusferrum opened Oct 19, 2026Contributor·

  ·
  41

• feat(List): occurrences and right-maximal repeats

  #1147·iosephusferrum opened Oct 19, 2026Contributor·

  ·

• feat(Logic): information order for Kleene

  #1142·jessealama opened Oct 16, 2026Contributor·1 task·

  ·

• feat(Logic): Kleene's strong three-valued logic

  #1140·jessealama opened Oct 16, 2026Contributor·

  ·

• feat(MultiTapeTM): tidiness is free at zero space

  #1138·crei opened Oct 15, 2026Collaborator·

  ·
  3

• feat(Circuit): strengthen Shannon's bound and drop finiteness assumptions

  #1130·SamuelSchlesinger opened Oct 13, 2026Collaborator·

  ·
  4

• feat(Languages): add probabilistic programs with typed oracles

  #1129·SamuelSchlesinger opened Oct 12, 2026Collaborator·9/9·

  ·
  8

• fix(CLL): take the idempotents of the fact 1 in phase semantics

  #1119·SamuelSchlesinger opened Oct 10, 2026Collaborator·

  ·

• fix(CLL): check both tensor premises in onlyAtomicAxioms

  #1118·SamuelSchlesinger opened Oct 10, 2026Collaborator·

  ·

• feat(MultiTapeTM): Complexity of iterated functions

  #1112·crei opened Oct 10, 2026Collaborator·

  ·

• feat(MultiTapeTM): Function composition for tidy computations

  #1111·crei opened Oct 10, 2026Collaborator·

  ·
  1

• refactor(LambdaCalculus): reorganize and cleanup in Untyped/Basic.lean

  #1096·pepamontero opened Oct 9, 2026Contributor·

  ·
  2