⚠ [8578/8632] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
ℹ [8589/8632] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [8592/8632] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [8596/8632] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
⚠ [8619/8632] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [8692/8705] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
ℹ [8694/8705] Replayed Research.Basic
info: Research/Basic.lean:40:0: Erdos796.Statement : Prop
⚠ [8696/8705] Replayed Research.CoreSidon
warning: Research/CoreSidon.lean:82:8: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/CoreSidon.lean:92:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8698/8705] Replayed Research.FiberTypes
warning: Research/FiberTypes.lean:57:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/FiberTypes.lean:78:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Research/FiberTypes.lean:98:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [8702/8705] Replayed Research.SemiprimeAsymptotic
info: Research/SemiprimeAsymptotic.lean:121:2: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: Research/SemiprimeAsymptotic.lean:182:43: Variable name `hC` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/SemiprimeAsymptotic.lean:917:6: 'push_cast' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [8703/8705] Replayed Research.UpperCombinatorics
warning: Research/UpperCombinatorics.lean:45:18: Variable name `hu` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/UpperCombinatorics.lean:45:45: Variable name `huW` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/UpperCombinatorics.lean:50:24: Variable name `husS` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/UpperCombinatorics.lean:51:5: Variable name `htpT` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Research/UpperCombinatorics.lean:99:0: automatically included section variable(s) unused in theorem `Erdos796.bipartiteRow_offDiag_eq`:
  [Fintype α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype α] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Research/UpperCombinatorics.lean:104:67: This simp argument is unused:
  and_assoc

Hint: Omit it from the simp argument list.
  simp [bipartiteRow, Finset.mem_offDiag, and_comm, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
Build completed successfully (8705 jobs).
PASS: authored sources are placeholder-free and Lean accepts the project
