⚠ [8579/8593] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
ℹ [8584/8593] Replayed Research.Basic
info: Research/Basic.lean:40:0: Erdos796.Statement : Prop
⚠ [8586/8593] 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`
⚠ [8588/8593] 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`
✔ [8592/8593] Built Research (3.2s)
Build completed successfully (8593 jobs).
PASS: authored sources are placeholder-free and Lean accepts the project
