[tunesmith]

Yes - currently, each argument/graph is independent, but I've designed it in a way that should be compatible with future plans to "transclude" parts of other public graphs. Like if some lemma is really valuable to your own unrelated argument, being able to include it.

I do think there's quite a lot that could be done with LLM assistance here, like finding "duplicate" candidates; statements with the same semantic meaning, for potential merge. It's really complicated to think through side effects though so I'm going slow. :)