Research · Lean sources
The proofs, file by file
Lean is a program that checks every step of a proof. These 14 files hold 556 checked theorems. A theorem shows that a conclusion follows from its stated assumptions, not that the assumptions describe a real company.
- CraftCosts.lean5 theorems · behind Lesson 1: When does doing it once beat doing it n times?
- ExpertiseScarcity.lean30 theorems · behind Lesson 2: Better expertise, worse fit
- StrategicPitch.lean51 theorems · behind Lesson 4: When everything is P1
- AdaptiveExploration.lean33 theorems · behind Lesson 5: What a record of failures is worth
- AssessmentLearning.lean42 theorems · behind Lesson 5: What a record of failures is worth
- AccessCommitment.lean47 theorems · behind Lesson 6: Making the truth worth telling
- RepeatedGame.lean56 theorems · behind Lesson 6: Making the truth worth telling
- AdaptiveSupport.lean37 theorems · behind Lesson 7: Teaching people, then stepping back
- PeopleDevelopment.lean48 theorems · behind Lesson 7: Teaching people, then stepping back
- ACMStaffing.lean24 theorems · behind Lesson 8: Generalists, specialists, queues and lulls
- WorkforcePlanning.lean35 theorems · behind Lesson 8: Generalists, specialists, queues and lulls
- WorkforceDevelopment.lean50 theorems · behind Lesson 9: Train, hire or contract
- CapabilityContinuity.lean53 theorems · behind Lesson 10: Who pays for the backup nobody needs today
- PreservationInvestment.lean45 theorems · behind Lesson 10: Who pays for the backup nobody needs today