# Terms of Service — lean4.party *Last updated: July 8, 2026* ## 1. Acceptance By accessing or using lean4.party (the "Service"), a Loogle/search instance for Lean 4 and Mathlib, you agree to these Terms of Service ("Terms"). If you do not agree, do not use the Service. ## 2. Nature of the Service The Service is provided by an individual, on a personal, non-commercial basis. It is not operated through a company, LLC, or other legal entity. There is no service-level agreement, support obligation, or guarantee of uptime. ## 3. No Warranty THE SERVICE IS PROVIDED "AS IS" AND "AS AVAILABLE," WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, TITLE, NON-INFRINGEMENT, ACCURACY, OR AVAILABILITY. NO WARRANTY IS MADE THAT THE SERVICE WILL BE UNINTERRUPTED, SECURE, ERROR-FREE, OR THAT SEARCH RESULTS WILL BE ACCURATE OR COMPLETE. ## 4. Limitation of Liability TO THE MAXIMUM EXTENT PERMITTED BY APPLICABLE LAW, THE OPERATOR SHALL NOT BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, CONSEQUENTIAL, EXEMPLARY, OR PUNITIVE DAMAGES, OR ANY LOSS OF DATA, PROFITS, OR GOODWILL, ARISING OUT OF OR RELATED TO YOUR USE OF, OR INABILITY TO USE, THE SERVICE, WHETHER BASED IN CONTRACT, TORT, STRICT LIABILITY, OR ANY OTHER LEGAL THEORY, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGES. YOUR SOLE REMEDY FOR DISSATISFACTION WITH THE SERVICE IS TO STOP USING IT. ## 5. No Guarantee of Availability The Service may be modified, suspended, or discontinued at any time, for any reason, without notice. ## 6. Acceptable Use You agree not to use the Service to: (a) attempt to disrupt, overload, or impair the Service or its infrastructure; (b) circumvent rate limits or access controls; (c) use the Service for any unlawful purpose. The operator reserves the right to block or rate-limit any user or IP address at their sole discretion. ## 7. Third-Party Content The Service may index or display content (e.g., Lean/Mathlib declarations, documentation) sourced from third-party repositories. The operator makes no claim of ownership over such content and disclaims responsibility for its accuracy or licensing status. ## 8. Indemnification You agree to indemnify and hold harmless the operator from any claims, damages, liabilities, and expenses (including legal fees) arising from your use of the Service or violation of these Terms. ## 9. Changes to These Terms These Terms may be updated at any time by posting a revised version at this URL. Continued use of the Service after changes constitutes acceptance. ## 10. Governing Law These Terms are governed by the laws of the operator's jurisdiction of residence, without regard to conflict-of-laws principles, except where mandatory local consumer-protection law requires otherwise. ## 11. Contact Questions about these Terms may be directed to `contact@lean4.party`.