Proof Sketch + Change proof to match sketch

seewoo5 / lean-poly-abc

Formalization of the proof of ABC conjecture for polynomials (Mason-Stothers theorem) in Lean 4

8 stars 0 forks source link

Proof Sketch + Change proof to match sketch #13

Closed jcpaik closed 1 year ago

jcpaik commented 1 year ago

A rewritten proof sketch. Current implementation does not follow this sketch. Refactoring the proof to this sketch might make the code much simpler.

seewoo5 commented 1 year ago

Why not adding it to readme?

jcpaik commented 1 year ago

Why not adding it to readme?

Because this proof is different from current implementation. Adding this to README at this point might trick readers to think that it is this version that we implemented. I'd like this to be merged after the code gets refactored.