Timeline for Lemma about splitting of homogeneous polynomial equations into irreducible equations
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 24, 2022 at 6:30 | comment | added | Junyan Xu | … Usually, the best way to catch errors in formalizing definitions and statements is to prove facts about the definitions and to use the statements in other proofs. | |
| Apr 24, 2022 at 6:28 | comment | added | Junyan Xu | The de Bruijn factor cs.ru.nl/~freek/factor is a price you have to pay when formalizing math; it depends on how complete the library (in this case the is_unit lemma and the factorization without multiplying by a unit are missing) and how intelligent automation is (look forward to more progress in AI which also learns from formalized math libraries!). However, once you formalize the definitions and statement and Lean checks the proof, then Lean guarantees that the statement is true, but it doesn't guarantee the definition and statement reflect what you have in mind. | |
| Apr 22, 2022 at 19:37 | comment | added | IV_ | Lean gives the result "No messages." That shows that all formulations are correct according to the Lean language. But how can we see if the proof is mathematically correct and effective? | |
| Apr 22, 2022 at 19:35 | comment | added | IV_ | The proof seems too complicated in comparison to the very simple mathematical proof. | |
| Apr 19, 2022 at 23:49 | comment | added | Junyan Xu |
@IV_ The first block of code needs the same import and open commands as in the second block to work. I edited the post to add them.
|
|
| Apr 19, 2022 at 23:47 | history | edited | Junyan Xu | CC BY-SA 4.0 |
added 103 characters in body
|
| Apr 19, 2022 at 20:23 | vote | accept | IV_ | ||
| S Apr 19, 2022 at 12:51 | review | First answers | |||
| Apr 19, 2022 at 17:26 | |||||
| S Apr 19, 2022 at 12:51 | history | answered | Junyan Xu | CC BY-SA 4.0 |