3:07 AM
@leslietownes I have no label. My latest label on MSE is to protect my privacy. I was catfished again or near-catfished. So this time doesn't count. It was for privacy reasons.
@XanderHenderson I guess for some people software grows on trees
@leslietownes basically, Ambroise et all took a liking to my YT videos when they were up on my diagram chaser pre-attempts. They were all focused on diagram editor and GUI, so when time it came to put together the gray area of "logic engine". I'm clueless. This time however, I've got it designed out to where we might see a proof of Snake Lemma in the first month of fully-functional release.
What is proof? There's no strict definition, so it's all about how we present it on the site. I preferably like blank screen (powerpoint like) presentation with as little content as possible. The Discord people are on the opposite end of that preference spectrum.
Okay there do exist some reasonable and strict definitions, however, mine is still kind of Wing it as I go along. There's always some advantage to seeing what your tech stack can actually handle algorithm wise before nailing down the final design
I ran into many issues with Neo4j's cypher caps.
But worked around them now
My definition of proof is if you can show it to some non-empty subset of accredited mathematicians, and they say yep that proves it to me. Then that is a proof. What about visual proofs of geometric identities? See it's very broad and what I meant to say is there's no all-emcompassing definition of proof.
If it works logically and people aren't deriving paradoxes too often, then I will be happy with the software. I think proof theory can be done relative to an area of math, so though our software is expressive enough to break in some area, or be too cludgy, not responsive enough, then we just say it's "geared for this other area of math."
But I'm trying to even support elementary expressions i.e. $f(x) \in R[x]$ but written out in any form that is common (like WolframAlpha or Geogebra input). But since it will be a proof engine. You can define your own rules that aren't too complicated. Because proofs are stored to the database, you can jump ahead once the database reaches a healthy size. Why step through what's already been both human and computer proof checked?
And if something simply can't be expressed, then you add it as an Axiom and that's it.
But the system is geared towards diagram-heads
So not for doing the analysis of twin prime theory, though you could try for basic stuff.
There's also stricter subclasses of Textual + Diagrammatic languages. These are more theoretically backed and so possess important properties the higher up more rigorous math requires. Mines more like a human-curated site.
After all, we can try to beautify the diagram that is the "Gluing" of two commuting diagrams along a common subdiagram, but the human is always going to want to touch it up as it's much easier to have that feature than to figure out how to beautify perfectly.
CD's are under-represented in math as far as listing of their properties formally. So substitution, gluing are best built-into-the backend code (hardcoded in a sense), while Functor of a triangle can be shown to the user as a username:Standard Library rule. You would have to apply this functor repeatedly and re-glue backtogether the various triangles to form the shape your after. That makes me want to make Functor also have built-in component.
As you can see you run into stuff actually just doing it than if you were to 100% plan ahead and no code until 100% designed.
Thata way you can functor a diagram with one-click instead of the fundamental crap (relative math!)
Functoring being in every-other paragraph of an arrow theory book
