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

{% block title %}
<title>Case study: Lean theorem prover community</title>
{% endblock %}

{% 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('zerver/for/lean-case-study.md') }}
            </div>
        </div>
    </div>
</div>

{% endblock %}