Timeline for Determining why my proof depends on the axiom of choice
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 18 at 22:46 | history | became hot network question | |||
| Feb 18 at 22:14 | answer | added | Robin Green | timeline score: 3 | |
| Feb 18 at 17:18 | comment | added | Andrej Bauer | You could tell us what you proved and we're going to guess where you used Dependent choice (and whether the use was necessary). | |
| Feb 18 at 14:54 | comment | added | Jason Rute | @Ricky. No. It is true in even base lean. Macros, automatic termination proofs, and common tactics can all add choice unexpectedly. | |
| Feb 18 at 12:37 | comment | added | Ricky | Well, if you start using a lot of mathlib then I agree, but otherwise it should be more or less fine. | |
| Feb 18 at 12:29 | comment | added | Jason Rute | I hate to say, this but the are many ways the axiom of choice can sneak into a Lean proof. Trying to do constructive math in Lean 4 is very painful. | |
| Feb 18 at 11:29 | comment | added | Ricky |
I would even start by replacing the full proof by sorry, to check that the statement doesn't somehow uses choice.
|
|
| Feb 18 at 11:28 | comment | added | Ricky |
Not a very elegant solution, but try to replace part of your proof by sorry and see what happens. Of course this will add sorry as an axiom, but at some point choice should disappear.
|
|
| S Feb 18 at 11:22 | review | First questions | |||
| Feb 19 at 1:51 | |||||
| S Feb 18 at 11:22 | history | asked | Robin Green | CC BY-SA 4.0 |