Suppose the following type is defined (C++ syntax, can be conceptually applied to any statically typed language.)

class T {
   int val;
   friend bool operator<(const T& lhs, const T& rhs) {
      return lhs.val < rhs.val;
   }
   // Ideally, if we should make them "friends"
   // Also, this doesn't make them belong to the type itself as they're not member functions
   friend bool operator>=(const T& lhs, const T& rhs) {
      return !(lhs < rhs);
   }
   // Also the following implementation is interesting
   friend bool operator>=(const T& lhs, const T& rhs) {
      return lsh.val >= rhs.val;
   }
};

So, the compiler can definitely check whether T supports operator< or operator>=, it can just look up the declaration.
This gets more complicated should these be defined as “friends” instead of member functions, but it can be done as far as I’m concerned.

However, can the compiler check whether the “common axiom of sorts” hold? (Can as in is it possible to check this in all scenarios? Doesn’t matter whether or not this would be standard-compliant.) Say:
not (a < b) == a >= b

Should we define one in terms of the other, it is definitely possible in this particular scenario, but this is naturally not the only axiom that needs to be checked, what about:
(a > b) => (b < a)
and it’s also not necessary (unfortunately) to define our behaviour in terms of something that has already been defined. And sometimes it wouldn’t be even possible.

So, if the compiler can check whether certain axioms hold, how? Generating random values from certain ranges? Is it possible to devise and proof correctness of such ranges?

This is mainly related to C++ concepts that unlike C++ concepts lite, should also be able to “support axioms”, whatever that means, I just can’t see a clear way as to how they can be enforced. Or will the creator of the type have to state what axioms his class obeys? C++ dropped the “concept maps” as far as I know.