if i pull the API for django or react or ...anything else, how much should i be expected to understand without any prior exposure? how is "domain-specific gibberish" any different? you make up words to represent groups of other words in order to capture concepts. it's literally just how language works.
let me translate for you:
proof assistant: program that checks your work (writing a proof) and helps you find new proofs.
synthetic: math where the axioms "represent" the objects instead of the other way around (they're "synthesized" from the objects)
1-category: a collection with objects and functions between them
2-category: a collection with objects, functions between them, and functions between those functions (called homotopies)
k-category: you get the idea
∞-category: the limit as k -> ∞
second-order abstract syntax which is great for lambda extraction: syntax specifically suited for this kind of stuff
and you know what? even though i am not a category theorist i was able to figure this out. you know how? i quickly skimmed the "docs" https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-c...
"In modern mathematics, an analytic theory is one whose basic objects are defined in some other theory, whereas a synthetic theory is one whose basic objects are undefined terms given meaning by rules and axioms"—Michael Shulman
In programming terms, I guess "synthetic" mathematics feels a bit like programming to an abstract interface.
https://ncatlab.org/nlab/show/synthetic+mathematics
In the first part of this video Cédric Villani gives (in French) a nice explanation of the distinction: https://youtu.be/xzVk56EKBUI?t=258
Edit: an English explanation, also by Villani: https://www.youtube.com/watch?v=AIrLXbwyYXQ
"I was looking for an experimental proof assistant for synthetic ∞-categories and stumbled across this awesome project..."
"It's wicked cool! It uses a version of second-order abstract syntax which is great for lambda extraction."
The project description sounds like something that MIT automated gibberish research paper generator would come up with.