Pull requests

• test(Tactic/Alias): cover alias with noncomputable section targets

  awaiting-review
  #2035·josaum opened Oct 21, 2026·

  ·
  1

  1

• chore: use meta imports for Lean in four tactic modules

  awaiting-review
  #2034·ChristianMurphy opened Oct 20, 2026·

  ·

• feat(List): add dropLast/getLast sum and product lemmas

  awaiting-reviewbreaks-mathlib
  #2030·CollinYuanjieRen opened Oct 16, 2026Contributor·

  ·
  1

• chore: don't re-export Batteries.Tactic.Basic from Batteries.Classes.Order

  awaiting-reviewbreaks-mathlib
  #2017·fgdorais opened Oct 9, 2026Collaborator·

  ·
  3

• feat(simpNF): flag dsimpable lemmas

  awaiting-reviewbreaks-mathlib
  #2011·JovanGerb opened Oct 6, 2026Contributor·

  ·
  1

• Pass adaptation title and message values without evaluating shell text

  awaiting-reviewbuilds-mathlib
  #2009·chessing234 opened Oct 5, 2026Contributor·

  ·
  1

• Stop adaptation creation when git merge fails without conflicts

  awaiting-reviewbuilds-mathlib
  #2008·chessing234 opened Oct 5, 2026Contributor·

  ·
  1

• Initialize adaptation arguments before selecting invocation mode

  awaiting-reviewbuilds-mathlib
  #2007·chessing234 opened Oct 5, 2026Contributor·

  ·
  1

• fix: handle empty files and filenames in whitespace lint

  awaiting-reviewbuilds-mathlib
  #2001·chessing234 opened Oct 1, 2026Contributor·

  ·
  1

• Proof of correctness for Array.equalSet

  awaiting-reviewbuilds-mathlib
  #1985·LordRatte opened Sep 27, 2026Contributor·

  ·
  2

• fix: resolve alias targets in the namespace of the alias name

  awaiting-reviewbuilds-mathlib
  #1982·fushanbobfan opened Sep 26, 2026·

  ·
  1

  1

• feat: report per-linter cost in runLinter --trace

  awaiting-reviewbuilds-mathlibmerge-conflict
  #1979·kim-em opened Sep 25, 2026Collaborator·

  ·
  2

• fix: ignore synthetic match terms in matchExpand code action

  awaiting-reviewbuilds-mathlib
  #1968·chessing234 opened Sep 16, 2026Contributor·1 of 2 tasks·

  ·
  1

  1

• feat: #do command

  awaiting-reviewbuilds-mathlib
  #1962·Rob23oba opened Sep 13, 2026Contributor·

  ·
  5

• feat: introduce Batteries Cell Network

  awaiting-reviewbuilds-mathlib
  #1955·fgdorais opened Aug 29, 2026Collaborator·

  ·
  1

• feat: prove/improve proof of [take,drop,splitAt,getElem?,getElem]_flatten

  awaiting-reviewbuilds-mathlib
  #1954·Bubbler-4 opened Aug 28, 2026·

  ·
  7

• feat(List): take/drop sum-prod lemmas and partialSums getLast?

  awaiting-authorbreaks-mathlib
  #1938·chessing234 opened Aug 3, 2026Contributor·1 task done·

  ·
  5

• feat: prove List.take_flatten

  awaiting-authorbuilds-mathlib
  #1919·MikeBoozer opened Jul 20, 2026·

  ·
  29

• Flake.nix

  awaiting-authormerge-conflict
  #1907·jmikedupont2 opened Jul 16, 2026·

  ·
  1

• feat(runLinter): --profile to report the slowest checks per linter

  builds-mathlibmerge-conflictWIP
  #1890·marcelolynch opened Jul 7, 2026Contributor·

  ·
  1

• chore: deprecate MLList in favour of Std.IterM

  merge-conflictWIP
  #1887·Seasawher opened Jul 5, 2026Contributor·

  ·

• feat: consume lake target specs in runLinter

  awaiting-reviewbuilds-mathlibmerge-conflict
  #1850·eric-wieser opened Jun 11, 2026Member·

  ·
  13

• refactor: consolidate linters

  awaiting-reviewbuilds-mathlibmerge-conflict
  #1830·fgdorais opened Jun 1, 2026Collaborator·

  ·
  23

• feat: add tape data structure

  awaiting-reviewbuilds-mathlib
  #1815·fgdorais opened May 23, 2026Collaborator·

  ·
  8

• feat: add basic byte order support

  breaks-mathlibWIP
  #1811·fgdorais opened May 18, 2026Collaborator·

  ·
  18