Thank you for feedback. Your last comment touched a very relevant point.
>From a tooling perspective, mmj2 for instance, do you think it would be possible to replace the ? for a &C1 and work on some proof elaboration steps that will produce the value for &C1, eventually promoting it to a hyp? Best regards. On Sunday, July 28, 2024 at 7:24:41 PM UTC+1 [email protected] wrote: > I would do something like this (which is not exactly metamath syntax but > not too hard to write precisely): > > 0 < k, > 0 < l, > F = (x e. RR |-> k*x^2 - 2*k*x + l), > { x | F(x) = 4 } = {A, B}, > (A - B)^2 + (F(A) - F(B))^2 = 6 > |- (A^2 + F(A)^2) + (B^2 + F(B)^2) = ? > > although to actually prove it you have to first fill in the ? with the > answer. > > On Sun, Jul 28, 2024 at 8:07 PM jagra <[email protected]> wrote: > >> Understand this is not a common, and probably not even wanted, topic on >> this group. >> >> Trying to translate to metamath a simple problem from AIMO train dataset, >> just out of curiosity. >> >> The problem statement is: >> >> Let $k, l > 0$ be parameters. The parabola $y = kx^2 - 2kx + l$ >> intersects the line $y = 4$ at two points $A$ and $B$. These points are >> distance 6 apart. What is the sum of the squares of the distances from $A$ >> and $B$ to the origin? >> >> Trying to come up a direct construction of the conditions and statement >> to prove and blocking, from my ignorance most certainly, on some >> embarassing road blocks. >> >> >> 1. Define function y=4 >> 2. Define parabola function in terms of k and l >> 3. Connect 1 & 2 with points A and B >> 4. Define distance between A and B >> 5. Define the goal in terms of A and B >> >> Really understand this is probably a basic question and I'm offsetting my >> due dilligence, so, no problem if no one takes the time to answer this :) >> >> Best regards, >> Jorge Agra >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/6f644425-c9fd-4516-b8f3-76b104c2be4fn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/6f644425-c9fd-4516-b8f3-76b104c2be4fn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b3b85824-1085-470e-848a-45e2b751f267n%40googlegroups.com.
