How do you know mathematicians lose track at this point? Is this an empirical observation?
-
-
-
⊢ x ∈ ⋂ (f : mv_polynomial (fin n) k) (H : f ∈ {u : mv_polynomial (fin n) k | ∃ (s : mv_polynomial (fin n) k) (H : s ∈ S) (t : mv_polynomial (fin n) k) (H : t ∈ T), u = s * t}), zeros f
- Još 1 odgovor
Novi razgovor -
-
-
[dilettante] ask lean to add user-defined syntactic sugar? could combine with a WYSIWYG LaTeX environment somehow? so you def a LaTeX --> Lean code map, and then you write the LaTeX, and the map compiles it, and the WYSIWYG makes it look nice
-
There is plenty of inbuilt user-defined syntactic sugar in Lean, I just can't get it to sugar this far. Maybe Lean 4 will be better in this regard. Some days I fret that I can't pull off notation tricks, other times I think "mathematicians should just learn the Lean syntax"
Kraj razgovora
Novi razgovor -
-
-
In my experience the translation of a textbook proof to a formal proof often requires some re-organization. For instance, you could prove instead that {x | x ∉ U ⇒ x ∈ V} is algebraic to avoid two cases and excluded middle, and get the union easily from that afterwards. (1/2)
-
You could show first that if x ∉ U then s(x) is invertible for some s ∈ S. Regarding an unwieldy statement in the middle, I don't see an immediate improvement. Proof assistants want you to engineer proofs a lot more carefully than humans do. (2/2)
- Još 3 druga odgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.