Is Euclid's Fourth Postulate Redundant?

Euclid's right-angle postulate excludes the existence of cone points: right angles at the vertex of a cone are smaller than right angles elsewhere on the cone. So this postulate cannot be proved insofar as the other axioms apply on a cone, which one could argue that they do.

Yes, Euclid Fourth postulate can be derived from (a modern formalization of) the other postulates and common notions. Our axiomatization includes the five line axiom, which corresponds to SAS.

We have machine checked proof of this fact. This work is described in this paper: https://arxiv.org/abs/1710.00787

The formal proof of the Fourth postulate can found in this file: https://github.com/GeoCoq/GeoCoq/blob/master/Elements/OriginalProofs/lemma_Euclid4.v

More readable proofs will come later.