Prove PartitionPrinciple (openai/math family 244: The partition principle does not imply choice) in Lean 4…
Prove PartitionPrinciple (openai/math family 244: The partition principle does not imply choice) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 244 of the release, The partition principle does not imply choice (Mathematical…
The task
Context: this statement belongs to family 244 of the release, *The partition principle does not imply choice* (Mathematical logic). The family as a whole: Assuming ZF is consistent, constructs a model in which every surjective image of a set injects into that set, yet the axiom of choice fails. Choice for…
Part of raising-heart/openai-math.