stat-lib · formal-stat · Jun 26, 2026 · Jun 26, 2026 · Jun 26, 2026
diff --git a/content/contribute.md b/content/contribute.md
@@ -5,7 +5,7 @@ intro: false
 
 # Contributing to Statlib
 
-Thank you for your interest in contributing to Statlib! Whether you are a statistician new to Lean, a Lean expert curious about statistics, or a CS / AI researcher interested in formalization tools, we are building with you. If anything in this document is unclear, please ask on the [Statlib Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib).
+Thank you for your interest in contributing to [Statlib](https://github.com/stat-lib/statlib)! Whether you are a statistician new to Lean, a Lean expert curious about statistics, or a CS / AI researcher interested in formalization tools, we are building with you. If anything in this document is unclear, please ask on the [Statlib Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib).
 
 ## Contents {#contents}
 
@@ -38,8 +38,8 @@ Statlib depends on Mathlib. We do not duplicate Mathlib's `MeasureTheory` or `Pr
 
 You are welcome to contribute in any way you see fit and have the most fun with.
 
-- **Propose something.** Open a GitHub issue describing what you would like to add, and mention it in the [Statlib Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib). We will discuss scope and placement before you invest heavily in code.
-- **Submit a pull request.** If you already have code you think fits Statlib, open a PR directly. See [Submitting a pull request](#submitting-a-pull-request) for what we expect.
+- **Propose something.** Open [a GitHub issue](https://github.com/stat-lib/statlib/issues/new/choose) describing what you would like to add, and mention it in the [Statlib Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib). We will discuss scope and placement before you invest heavily in code.
+- **Submit a pull request.** If you already have code you think fits Statlib, [open a PR](https://github.com/stat-lib/statlib/pulls) directly. See [Submitting a pull request](#submitting-a-pull-request) for what we expect.
 - **Join an active working group.** Browse current projects on our website and the corresponding Zulip topics.
 - **Discuss.** Join the [Statlib Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib); there are open questions you may be able to help with.
 - **Propose a project.** We particularly welcome statisticians whose research vision could anchor a sustained working group, especially authors of widely used textbooks and lecture notes. Advising on definitions and levels of abstraction, reviewing what gets formalized, and catching when a Lean statement drifts from the source statistics are all highly desired contributions.

diff --git a/content/index.md b/content/index.md
@@ -6,7 +6,7 @@ intro: false
 
 # Statlib
 
-Statlib provides the foundational framework for classical, contemporary, and emerging research in mathematical statistics. Drawing deeply from diverse domains, including real, functional, and convex analysis, measure theory, stochastic calculus, combinatorics, probability, and information theory, theoretical statistics demands absolute precision. As LLM-generated proofs become increasingly prevalent across these sub-disciplines, the need for rigorous, machine-verified mathematical theories has never been more urgent. While Lean's Mathlib is structured for broad mathematical domains, Statlib leverages its rich API ecosystem to deliver a streamlined, specialized library dedicated exclusively to theoretical statistics.
+[Statlib](https://github.com/stat-lib/statlib) provides the foundational framework for classical, contemporary, and emerging research in mathematical statistics. Drawing deeply from diverse domains, including real, functional, and convex analysis, measure theory, stochastic calculus, combinatorics, probability, and information theory, theoretical statistics demands absolute precision. As LLM-generated proofs become increasingly prevalent across these sub-disciplines, the need for rigorous, machine-verified mathematical theories has never been more urgent. While Lean's Mathlib is structured for broad mathematical domains, Statlib leverages its rich API ecosystem to deliver a streamlined, specialized library dedicated exclusively to theoretical statistics.
 
 Development begins with the core foundations of statistical inference within decision-theoretic and local asymptotic-theory frameworks. However, the library's architecture is explicitly designed for dynamic growth, scaling to encompass nonparametric and semiparametric statistics, alongside modern frontiers such as high-dimensional statistics, conformal inference, and frameworks for information-theoretic and computational trade-offs.
 

diff --git a/contribute.html b/contribute.html
@@ -23,7 +23,7 @@
 <main>
   <div class="wrap">
     <h1>Contributing to Statlib</h1>
-    <p>Thank you for your interest in contributing to Statlib! Whether you are a statistician new to Lean, a Lean expert curious about statistics, or a CS / AI researcher interested in formalization tools, we are building with you. If anything in this document is unclear, please ask on the <a href="https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib" target="_blank" rel="noopener">Statlib Zulip channel</a>.</p>
+    <p>Thank you for your interest in contributing to <a href="https://github.com/stat-lib/statlib" target="_blank" rel="noopener">Statlib</a>! Whether you are a statistician new to Lean, a Lean expert curious about statistics, or a CS / AI researcher interested in formalization tools, we are building with you. If anything in this document is unclear, please ask on the <a href="https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib" target="_blank" rel="noopener">Statlib Zulip channel</a>.</p>
     <h2 id="contents">Contents</h2>
     <ul>
     <li><a href="#about-statlib">About Statlib</a></li>
@@ -49,8 +49,8 @@ <h2 id="relationship-to-mathlib">Relationship to Mathlib</h2>
     <h2 id="how-to-contribute">How to contribute</h2>
     <p>You are welcome to contribute in any way you see fit and have the most fun with.</p>
     <ul>
-    <li><strong>Propose something.</strong> Open a GitHub issue describing what you would like to add, and mention it in the <a href="https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib" target="_blank" rel="noopener">Statlib Zulip channel</a>. We will discuss scope and placement before you invest heavily in code.</li>
-    <li><strong>Submit a pull request.</strong> If you already have code you think fits Statlib, open a PR directly. See <a href="#submitting-a-pull-request">Submitting a pull request</a> for what we expect.</li>
+    <li><strong>Propose something.</strong> Open <a href="https://github.com/stat-lib/statlib/issues/new/choose" target="_blank" rel="noopener">a GitHub issue</a> describing what you would like to add, and mention it in the <a href="https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib" target="_blank" rel="noopener">Statlib Zulip channel</a>. We will discuss scope and placement before you invest heavily in code.</li>
+    <li><strong>Submit a pull request.</strong> If you already have code you think fits Statlib, <a href="https://github.com/stat-lib/statlib/pulls" target="_blank" rel="noopener">open a PR</a> directly. See <a href="#submitting-a-pull-request">Submitting a pull request</a> for what we expect.</li>
     <li><strong>Join an active working group.</strong> Browse current projects on our website and the corresponding Zulip topics.</li>
     <li><strong>Discuss.</strong> Join the <a href="https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib" target="_blank" rel="noopener">Statlib Zulip channel</a>; there are open questions you may be able to help with.</li>
     <li><strong>Propose a project.</strong> We particularly welcome statisticians whose research vision could anchor a sustained working group, especially authors of widely used textbooks and lecture notes. Advising on definitions and levels of abstraction, reviewing what gets formalized, and catching when a Lean statement drifts from the source statistics are all highly desired contributions.</li>

diff --git a/index.html b/index.html
@@ -24,7 +24,7 @@
 <main>
   <div class="wrap">
     <h1>Statlib</h1>
-    <p>Statlib provides the foundational framework for classical, contemporary, and emerging research in mathematical statistics. Drawing deeply from diverse domains, including real, functional, and convex analysis, measure theory, stochastic calculus, combinatorics, probability, and information theory, theoretical statistics demands absolute precision. As LLM-generated proofs become increasingly prevalent across these sub-disciplines, the need for rigorous, machine-verified mathematical theories has never been more urgent. While Lean&#x27;s Mathlib is structured for broad mathematical domains, Statlib leverages its rich API ecosystem to deliver a streamlined, specialized library dedicated exclusively to theoretical statistics.</p>
+    <p><a href="https://github.com/stat-lib/statlib" target="_blank" rel="noopener">Statlib</a> provides the foundational framework for classical, contemporary, and emerging research in mathematical statistics. Drawing deeply from diverse domains, including real, functional, and convex analysis, measure theory, stochastic calculus, combinatorics, probability, and information theory, theoretical statistics demands absolute precision. As LLM-generated proofs become increasingly prevalent across these sub-disciplines, the need for rigorous, machine-verified mathematical theories has never been more urgent. While Lean&#x27;s Mathlib is structured for broad mathematical domains, Statlib leverages its rich API ecosystem to deliver a streamlined, specialized library dedicated exclusively to theoretical statistics.</p>
     <p>Development begins with the core foundations of statistical inference within decision-theoretic and local asymptotic-theory frameworks. However, the library&#x27;s architecture is explicitly designed for dynamic growth, scaling to encompass nonparametric and semiparametric statistics, alongside modern frontiers such as high-dimensional statistics, conformal inference, and frameworks for information-theoretic and computational trade-offs.</p>
     <p>To support this vision, our workflow centers on coordinating targeted formalization projects across both classical and modern methods, developing comprehensive tutorials to onboard future contributors, and establishing a collaborative forum to address shared architectural themes and implementation challenges.</p>
     <p>We would like to thank <a href="https://www.contrib.andrew.cmu.edu/~avigad/" target="_blank" rel="noopener">Jeremy Avigad</a> (Carnegie Mellon University) and <a href="https://remydegenne.github.io/" target="_blank" rel="noopener">Rémy Degenne</a> (Inria center at the University of Lille) for support and encouragement in the process of initiating and developing this library.</p>