Can't = compare axioms?

Stream: general

[Marvin]

I define an axiom which many other expressions will reduce down to. In this case I make a trivial synonym

axiom p : Prop
abbrev q := p
#eval p = q

I get

failed to compile definition, compiler IR check failed at `_eval`. Error: depends on declaration 'Prop.linearOrder', which has no executable code; consider marking definition as 'noncomputable'```
Why is this?

[Kevin Buzzard]

If we could #eval props then we could figure out if the Riemann Hypothesis is true by #eval RiemannHypothesis = True

[Kevin Buzzard]

As has been suggested to you in another thread, you probably want to make your own computable Formula type rather than using Lean's Prop universe.