Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Hildreth.lean
SHA-256: 8e842fa275d76c090c5bc1e834e291785a2e48c7a7917ebc64c421f2c1bdb153
Result: passed

'PaperToLean.Hildreth.move_at' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Hildreth.move_other' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Hildreth.objective_change' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Hildreth.coordinate_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Hildreth.step_feasible' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Hildreth.coordinate_optimal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Hildreth.step_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Hildreth.sweep_guarantee' depends on axioms: [propext, Classical.choice, Quot.sound]
