@F.Zer: I just realized that I made a careless error in my claimed proof of the existence of sqrt(2) in ℝ. Lol... I'm feeling lazy now so let me know when you want a correct proof. Of course, you're also welcome to find the error.

And there is atleast 3 red edges or atleast 3 green edges connected to "a" because in this case, we have at least 5 other nodes besides "a".

@user21820 As a start, I will focus only in the "hard case" of triangle inequality proof, if that is ok. What do you think ?

∀ x,y ∈ ℝ ( abs(x+y) ≤ abs(x) + abs(y) ) [triangle]
  ∀ x,y ∈ ℝ( x·x = y·y ⇒ x = y )
  ∀ x ∈ ℝ ( abs(x)^2 = x^2 )
  Given x,y ∈ ℝ:
    If x ≥ 0 ∧ y < 0:
      x·y ≤ 0
      4·x·y ≤ 0
      2·x·y ≤ –2·x·y
      x^2+2·x·y+y^2 ≤ x^2–2·x·y+y^2
      (x+y)^2 ≤ (x–y)^2
      abs(x+y)^2 ≤ (x–y)^2
      abs(x+y) ≤ x–y
      abs(x) = x
      abs(y) = –y
      abs(x+y) ≤ abs(x) + abs(y)
    ...
    abs(x+y) ≤ abs(x) + abs(y)
  ∀ x,y ∈ ℝ ( abs(x+y) ≤ abs(x) + abs(y) )

@Prithubiswas Excellent!

@Prithubiswas And your diagrams are precisely the kind of diagrams that I was hoping you would come up with! =)

@Prithubiswas And yes that is the elegant solution. Equivalently, if you do the entire proof by contradiction, then the conditions say that there is no triangle at all, and so you only need the two implications shown on the left in your diagrams. Applying both of them to some vertex a, either it has 3 red or 3 green edges and hence a contradiction.

So, now all that remains is to translate that argument into an FOL proof.

Note that in the subcontext where the conditions and negation of the conclusion hold, after picking some vertex a, your first implication can be expressed as a lemma of the form ∀x,y,z ( a,x,y,z are distinct and c(a,x),c(a,y),c(a,z) are all true ), and similarly your second implication is ∀x,y,z ( a,x,y,z are distinct and c(a,x),c(a,y),c(a,z) are all false ). So you can first prove these lemmas and then use them multiple times to reach a contradiction in the pure FOL proof.

@F.Zer That's an unusual idea. Did you check your deduction of "abs(x+y) ≤ x–y"?

@user21820 I will check and come back.

However, that's not the 'right' solution. There is no need to use multiplication at all. If y < 0 ≤ x, then why can't you figure out what abs(x−y) is just by definition and a simple deductive step?

@user21820 Thanks for the insight. I hope you realise I am trying hard to not be so rigid in my attempts and "think out of the box" :-)

I will attempt your suggestion.

Yes that's good, hence the quote-marks around "right".

Good !

However, you should also do a breadth-first search. It won't do to miss a 1-step proof and end up with a 20-step proof.

@user21820 That's very interesting ! What do you mean by "breadth-first search" ?

I thought you are a programmer?

@user21820 I don't have the graphs math background. I very recently started working with trees in Haskell :-)

Check wikipedia. Every programmer ought to know it, along with depth-first search.

In College, we barely touched on the subject. I will check Wikipedia.

It has nothing to do with graphs per se, even though it is natural to represent a BFS search via a search tree.

@user21820 I just read it and I think I got the point. Could you tell me now what's the practical use you had in mind related to proofs ?

I have to go out a moment. See you !

You should try not only what you think is a promising approach but also check what you can get within a few steps.

See you!

@user21820 Oh, excellent !

∀ x,y ∈ ℝ ( abs(x+y) ≤ abs(x) + abs(y) ) [triangle]
  Given x,y ∈ ℝ:
    If x ≥ 0 ∧ y < 0:
      x·y ≤ 0
      4·x·y ≤ 0
      2·x·y ≤ –2·x·y
      x^2+2·x·y+y^2 ≤ x^2–2·x·y+y^2
      (x+y)^2 ≤ (x–y)^2
      abs(x+y)^2 ≤ (x–y)^2
      If abs(x+y) > x–y:
        –y > 0
        x–y > 0
        abs(x+y)^2 > (x–y)^2
        ⊥
      abs(x+y) ≤ x–y
      abs(x) = x
      abs(y) = –y
      abs(x+y) ≤ abs(x) + abs(y)
    ...
    abs(x+y) ≤ abs(x) + abs(y)
  ∀ x,y ∈ ℝ ( abs(x+y) ≤ abs(x) + abs(y) )

@user21820 I checked and fixed it.

I will do the other thing you proposed when this approach is ready.

Guess what, I was talking nonsense above.

That's fine !

Get your approach working first. The better approach is not using abs(x−y); I have no idea why I thought we should care about abs(x−y)...

@user21820 Good. What do you think about my most recent attempt. Is it correct ?

Should I fill the remaining "..." ?

@F.Zer Yes it is correct. The other case is almost symmetrical, right?

The better approach is:

If y < 0 ≤ x:
  If x+y ≥ 0:
    abs(x+y) = x+y < x−y = abs(x)+abs(y).
  If x+y < 0:
    abs(x+y) = ... [equally easy]

@user21820 Of course. In many proofs, I have seen "WLOG" in such cases. What's your preferred way of doing this (in a formal way) ? You have shown me different forms, in the past months. I am wondering what you do when one proof is the same as other only with two variables interchanged.

@user21820 That's very nice. As soon as I finish mine, I will attempt it.

@F.Zer You would need to factor the subproofs. If the subproofs are too short to justify factoring, then just copy-paste and modify.

@user21820 Thank you. I appreciate it.

If it is truly a swap, you could prove a lemma and use it twice.

That's great !

That seems to be the case here, so it works. After all, your subproof just needs one more line to yield ∀x,y∈ℝ ( y < 0 ≤ x ⇒ abs(x+y) ≤ abs(x)+abs(y) ). So it seems worth it here.

@user21820 One question: suppose the case it is truly a swap but yields a very insignificant fact. Would you prove a lemma, in that case ?

In a random proof, I mean.

@user21820 That's really fantastic.

∀ x,y ∈ ℝ ( abs(x+y) ≤ abs(x) + abs(y) ) [triangle]
  ∀x,y∈ℝ ( y < 0 ≤ x ⇒ abs(x+y) ≤ abs(x)+abs(y) ) [lemma]
  Given x,y ∈ ℝ:
    If x ≥ 0 ∧ y ≥ 0:
      x+y ≥ 0
      abs(x) = x ∧ abs(y) = y
      abs(x+y) = x+y
      abs(x+y) = x+y = abs(x)+abs(y)
      abs(x+y) ≤ abs(x) + abs(y)
    If x < 0 ∧ y < 0:
      x+y < 0
      abs(x) = –x ∧ abs(y) = –y
      abs(x+y) = –x–y
      abs(x+y) = –x–y = abs(x)+abs(y)
      abs(x+y) ≤ abs(x) + abs(y)
    If y < 0 ≤ x:
      abs(x+y) ≤ abs(x) + abs(y) [lemma]

@user21820 This is the full proof.

@F.Zer Can't you just prove it before the main proof? If it's only used only somewhere inside you should of course prove it inside before it is used twice.

@F.Zer Where is your proof of the lemma anyway?

@user21820 I am finishing it :-)

@F.Zer So I don't see why you should separate the two.

@user21820 That is exactly what I was looking for. I appreciate it.

∀ x,y ∈ ℝ ( abs(x+y) ≤ abs(x) + abs(y) ) [triangle]
  Given x,y ∈ ℝ:
    If y < 0 ≤ x:
      If x+y ≥ 0:
        abs(x+y) = x+y < x−y = abs(x)+abs(y).
      If x+y < 0:
        –x ≤ x
        –x–y ≤ x–y
        abs(x+y) = –x–y
        abs(x+y) = –x–y ≤ x–y = abs(x)+abs(y)
      abs(x+y) ≤ abs(x)+abs(y)
  ∀x,y∈ℝ ( y < 0 ≤ x ⇒ abs(x+y) ≤ abs(x)+abs(y) )
  Given x,y ∈ ℝ:
    If x ≥ 0 ∧ y ≥ 0:
      x+y ≥ 0
      abs(x) = x ∧ abs(y) = y
      abs(x+y) = x+y
      abs(x+y) = x+y = abs(x)+abs(y)
      abs(x+y) ≤ abs(x) + abs(y)

So you're done.

Good !

@F.Zer Do whatever you think will get you a nice proof fastest.

@user21820 Ok, I feel like stopping and proving every lemma breaks the flow of proving the main proof.

Just wondered about your preferred way.

@F.Zer Well... you're right. But the system is not one where you can put lemma later... It's not aesthetically designed...

Anyway, I'm going off now.

@user21820 Yes, of course. But I can simply hit a keyboard shortcut and move the lemmas to the top.

@user21820 Have a nice day and thank you for your help ! See you !

I was wondering if someone could help me with this question: math.stackexchange.com/questions/4235224/…

@user21820 I realise that I never formalised Q10 into FOL. Since I do not want to spoil the solution, can I post my working draft perhaps in another room or some other form of communication ? What would you prefer ?