What is a Lurch Site?
The problem Lurch Sites solve
While it's true that anyone can try Lurch online right now, that copy of the app is the "plain vanilla" version, which means:
- it has the default configuration (just one of many possible ways to configure the app), and
- it does not include any example mathematical definitions, axioms, or theorems, so you can do only very tiny and uninteresting proofs.
We cannot solve this problem just by adding to that app a lot of documents that define interesting mathematics, because every author has a different style, a different set of preferred topics, a different way of teaching. We do not want to force any one style or set of axioms on the user.
How Lurch Sites solve that problem
The link above, which goes to the "plain vanilla" version of the app, should not be considered the definitive copy of the app; rather, there is no definitive copy. We allow anyone with a GitHub account to fork that repository and, in that fork, configure the app to their own preferences. They can also upload whatever mathematical documents they've authored into that new repository. Then if they enable web access to that repository, they will have a copy of Lurch running that behaves the way they want and includes the mathematics that they want. We call such a repository a Lurch Site.
We maintain on this website a gallery of Lurch Sites, so that new users don't need to create their own Lurch Site, but might find that someone has already built what they need. If you create a Lurch Site, let us know so that we can include it in the gallery! Just create a new issue for this website repository and say that you want to add your Lurch Site to the gallery, providing the URL.