Condiciones de servicio
1. Lo que hace el servicio
Usted presenta una reclamación y una norma. Lo ejecutamos pasado un panel de modelos de IA que usted selecciona, más un modelo de árbitro que las reglas sobre criterios de aceptación, y tratamos de formalizar el resultado en Lean 4 contra Mathlib. La salida es una transcripción, un conjunto de resoluciones, un veredicto, y donde se intentó formalizar, el resultado Lean.
2. ¿Cuál es y no es la salida
La salida se genera mediante modelos de IA de terceros y no es un consejo. No es asesoramiento legal, médico, financiero, de ingeniería o profesional de ningún tipo, y no se crea ninguna relación profesional mediante el uso de este servicio.
El árbitro que dicta un criterio cumplido es una declaración sobre la evidencia registrada en ese partido. No es una garantía de corrección. Los modelos de IA cometen errores, malentienden fuentes, y pueden fabricar citas a pesar de las instrucciones no hacerlo. Debe verificar independientemente cualquier cosa en la que pretenda confiar, particularmente antes de publicarla, presentarla o actuar en ella. Esta es una herramienta para el trabajo de prueba de presión, no un sustituto de la revisión humana calificada.
Una formalización Lean exitosa significa que el núcleo Lean aceptó una prueba de la declaración que fue formalizada, en contra de la versión de Mathlib en uso en ese momento. No significa que la declaración sea una traducción fiel de lo que usted pidió, y elegir una declaración formal que no diga lo que usted quiso decir es la manera más común en que un resultado formal engaña. Lea la declaración formal, no sólo el veredicto.
3. Su contenido
Usted mantiene la propiedad de las reclamaciones que presenta y de la salida producida para usted. Nos concede sólo la licencia necesaria para operar el servicio: procesar su envío, transmitirlo a los proveedores de modelos que seleccionó, y almacenar el partido resultante para que pueda volver a él.
Los partidos son privados por defecto. Si marca un partido público, se hace visible para cualquier persona con el enlace y puede aparecer en nuestra galería pública. No publique un partido que contenga nada confidencial.
No envíe datos personales sobre otros, material confidencial que no tenga derecho a compartir, o contenido que sea ilegal.
4. Créditos y facturación
El crédito es prepago y se consume como partido. Cada partido tiene un límite de gasto que usted establece; alcanzarlo pausa el partido en lugar de continuar gastando. Los saldos no son transferibles y, excepto cuando lo requiera la ley, no son reembolsables una vez consumidos. El crédito no utilizado es reembolsable bajo petición.
Si conecta su propia clave de inferencia, pague a su proveedor directamente y no le facturamos ningún cargo por token. Pasado el pago de la asignación gratuita indicada se aplica una tasa de infraestructura para cubrir la ejecución del panel, herramientas y almacenamiento.
Podemos cambiar los precios con aviso. Los cambios nunca se aplican al crédito ya adquirido.
5. Uso aceptable
No utilice el servicio para generar contenido que dañe a otros, para intentar extraer nuestras instrucciones o instrucciones del sistema, para eludir los límites de gasto o tasa, o para revender el acceso sin un acuerdo escrito. La herramienta de ejecución de código es para verificar reclamaciones; no lo use para atacar ningún sistema.
6. Disponibilidad
Dependemos de proveedores de modelos de terceros. Los proveedores bajan, cambian los modelos y los depreda. Un partido interrumpido por cualquier razón se pausa y se puede reutilizar; no cobramos por el trabajo que no ocurrió. No garantizamos disponibilidad ininterrumpida, y un modelo que usted utilizó antes puede no estar disponible.
7. Responsabilidad
En la medida más completa permitida por la ley, el servicio se proporciona como es sin garantías de ningún tipo. Nuestra responsabilidad total por cualquier reclamación se limita a la cantidad que nos pagó en los tres meses anteriores a la reclamación surgió. No somos responsables de la pérdida indirecta o consecuencia, incluyendo cualquier pérdida derivada de la dependencia de la producción modelo.
8. Terminación
Puede cerrar su cuenta en cualquier momento; le devolveremos el crédito no utilizado. Podemos suspender las cuentas que infrinjan estos términos o que pongan en riesgo el servicio.
9. Cambios, idioma y contacto
Podemos actualizar estos términos; los cambios materiales se anunciarán en el sitio.
Las traducciones de esta página se proporcionan por conveniencia y se producen automáticamente. Cuando una traducción y la versión en inglés difieren, la versión en inglés rige.
Preguntas: Contáctenos.