{% extends "zerver/portico.html" %}
{% set entrypoint = "landing-page" %}

{% set PAGE_TITLE = "Case study: Lean theorem prover community | Zulip" %}
{% set PAGE_DESCRIPTION = "Zulip enables collaboration at scale: “We could never do what we’re doing on Slack or Discord.”" %}

{% block customhead %}
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
{% endblock %}

{% block portico_content %}

{% include 'zerver/landing_nav.html' %}

<div class="portico-landing why-page solutions-page case-study-page">
    <div class="hero bg-education">
        <div class="bg-dimmer"></div>
        <div class="content">
            <h1 class="center">Case study: <br/>Lean theorem prover community</h1>
        </div>
        <div class="hero-text">
            Learn more about using Zulip for <a href="/for/research/">research</a><br/>
            and <a href="/for/open-source/">open source</a> communities.
        </div>
    </div>
    <div class="main">
        <div class="padded-content">
            <div class="inner-content markdown">
                {{ render_markdown_path('corporate/case-studies/lean-case-study.md') }}
            </div>
        </div>
    </div>
</div>

{% endblock %}