Posted by alice balice on Sep 21st 26 at 6:27 AM

I'd start by making each relation instance its own node, with named links to its arguments. So f : A → B becomes a relation node connecting f, A and B, with roles like “function,” “domain” and “codomain.” You can represent a hyperedge that way in an ordinary graph database. W3C has a useful n-ary relation pattern for this.

For your custom ontology, give each relation type a definition: which arguments it accepts, their types, whether order matters, and what assumptions apply. Otherwise “any relation I want” can get ambiguous pretty quickly, especially with variables and quantifiers.

The bigger question is what you mean by rigorous. Checking that a relation has the right structure is one thing, checking that a mathematical claim follows from its assumptions is another. If you want checked proofs, I'd look at Lean and have the graph link to formal definitions and proofs. Keep conjectures, axioms and proved statements distinguishable too.

Are you mainly trying to organize mathematical knowledge, or have the system verify deductions?