It’s probably not important.

I’m concerned about

it reminded me of set theory, but thinking about it more, it ended up merely resembling it

When did it diverge?

Can your system express sets that have multiple parent sets? Can israelifarmers be inside of both earth/middleeast/israel/farmers/ and in work/primaryindustry/agriculture/horticulture?

I think in the design of systems like these there’s often a tension between tag heirarchy and tag intersection as a way of talking about increasingly specific categories, and intersection should be used more often than it currently is. Under intersection, as long as the “israeli” and “farmer” categories exists, “israeli∧farmer” category exists implicitly as a subset of israeli and farmer, and there is no ambiguity as to where it should “go”.

I’ve always wondered why there isn’t more interest in automated provers. What happens when you make a term-rewriting system with a taste for symmetric, interrelated systems of theorems and have it just search for proofs (and shorter versions of those proofs) for a few years? Do fully artificial mathematicians ever come up with novel theorems? Are they any good at condensing proofs enough that they become comprehensible to humans?

Edit: Had a cursory look through lesswrong history

https://www.lesswrong.com/posts/uu9EAiFwoYg76AAEe/progress-on-automated-mathematical-theorem-proving#hqQJuwRnrESYSomuB

A post by JonahSinick from Jul 2013, asking the very question

Progress on automated mathematical theorem proving?https://www.lesswrong.com/posts/w9Wx3PXSCfZFCGxff/discussion-of-concrete-near-to-middle-term-trends-in-ai#ArmbHFn62E24HRShs

https://www.lesswrong.com/posts/uu9EAiFwoYg76AAEe/progress-on-automated-mathematical-theorem-proving#hqQJuwRnrESYSomuB

The competition still seems to be active. Last year’s winners were Satallax 3.3, Vampire 4.3 (in three categories), iProver 2.8, and MaLARea 0.6