3 ms·

thanks. that's really not the IMO though, is it? coming up with a formal representation is a large part of the challenge, isn't it?

• im3w1l 6y ago
  ∀n∈Z: n>=3 => ∃S∈(R^2)^n: [~∃p1∈S ∃p2∈S ∃p3∈S ∃a∈R: p1!=p2 & p2 != p3 & p3 != p1 & p1 + a(p2-p1) = p3] & [~∃p1∈S ∃p2∈S ∃a∈Z ∃b∈Z: |p1-p2| = a/b] & [∀p1∈S ∀p2∈S ∀p3∈S ∃a∈Z ∃b∈Z p1!=p2 & p2 != p3 & p3 != p1 => Area(p1, p2, p3) = a / b] So far it's pretty much mechanical∗. The big question is how you will formalize Area(p1, p2, p3). Heron's could possibly make the problem much harder than cross product. ∗Although I may have made some or many mistakes.