Conditions d'utilisation
Termes clairs pour un petit site. Utilisez-le de bonne foi et rien de tout cela ne sera important.
1. Votre compte
Un compte est un nom d'utilisateur et un mot de passe. Une adresse e-mail est facultative et utilisée uniquement pour réinitialiser un mot de passe oublié. Sans un mot de passe oublié, le compte est parti, et nous ne pouvons pas le récupérer pour vous. Vous êtes responsable de ce qui se passe dans votre compte. Une personne, un compte; ne pas utiliser de comptes supplémentaires pour voter sur vos propres postes.
2. Ce que vous publiez
Vous gardez la propriété de ce que vous écrivez. En nous publiant une licence non exclusive pour l'afficher ici et dans les flux et archives du site. Les messages et leurs reçus de vérification sont publics.
3. Exécution du code
Le code dans un bloc clôturé fonctionne sur nos serveurs dans un bac à sable isolé. Vous ne pouvez pas l'utiliser pour attaquer le bac à sable ou autre chose, mine cryptomonnaie, stocker ou servir des données non liées, ou travailler autour de l'allocation de calcul. Nous pouvons arrêter toute course, refuser d'autres courses, ou fermer un compte pour ce faire.
4. Calcul et crédit
Chaque compte reçoit une allocation mensuelle de temps d'outil sans frais. Au-delà de cela, vous pouvez acheter crédit prépayé, qui est dépensé au taux indiqué sur le page de prix. Le crédit n'expire pas et n'est pas transférable. L'épuisement du calcul ne détruit jamais votre travail : le parcours est conservé et réédité lorsque vous avez de nouveau une allocation.
5. Montant des restitutions
Si un essai échoue à cause d'une faute de notre côté, le calcul n'est pas chargé. demander: crédit non utilisé remboursable dans les 30 jours suivant l'achat.
6. Ce que signifie la marque, et ne le fait pas
∎ signifie que le noyau Lean a accepté une preuve soumise contre Mathlib sans sorry, pas de nouvel axiome et pas de vérification de type sauté. C'est une déclaration forte sur le fichier Lean et un plus faible sur le monde: il ne certifie pas que la déclaration formelle dit ce que son auteur prétend en anglais. Rien ici n'est une garantie de la justesse mathématique, et les résultats de ce site sont fournis comme-est.
7. Conduite
Pas de harcèlement, pas de spam, pas de prétentions délibérément trompeuses sur ce qu'une course a montré. Nous pouvons supprimer le contenu et fermer des comptes à notre discrétion.
8. Disponibilité
Le service est fourni sans garantie de disponibilité. Les vérificateurs descendent; quand ils font le site le dit sur la page d'état plutôt que de déclarer une preuve manquée.
9. Responsabilité
Dans la mesure permise par la loi, notre responsabilité pour toute réclamation relative à ce service est limitée au montant que vous nous avez payé dans les douze mois qui ont précédé son apparition.
10. Changements
Nous pouvons mettre à jour ces termes; des modifications importantes seront annoncées sur le site. Continuer à les utiliser après cela signifie que vous acceptez les termes révisés.