diff --git a/README.md b/README.md
index 1550049c..d28a47c4 100644
--- a/README.md
+++ b/README.md
@@ -253,6 +253,7 @@ Any other questions? Please check out our [FAQ](./FAQ.md), and if your question
     * [Scala](#scala)
     * [Zig](#zig)
   * [Proof Assistants](#proof-assistants)
+    * [Alternatives](#proof-assistants-alternatives)
   * [Remote Desktop](#remote-desktop)
   * [Reverse Engineering and Debugging](#reverse-engineering-and-debugging)
   * [RSS](#rss)
@@ -2603,11 +2604,17 @@ Note that Scala (except version 2 and up to 3.3.7 LTS) is itself tainted; see [t
 
 ## Proof Assistants
 
-| Name | Last Untainted Version or Commit ID | Tags and Evidence | Alternative(s) |
+| Name | Last Untainted <br /> Version/Commit ID | Evidence | Alternative(s) | 
 |---|:---:|---|---|
 | [Agda](https://github.com/agda/agda) | [`2.8.0`](https://github.com/agda/agda/releases/tag/v2.8.0) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/agda/agda/pull/8507)) | [Mikan](https://codeberg.org/1lab/mikan) |
-| [Lean](https://leanprover-community.github.io/) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/leanprover/lean4/tree/master/.claude), [2](https://github.com/leanprover/lean4/pull/12776)) <br /> [![AI sponsored](./badges/ai-sponsored-blue.svg)](#sponsored-by-ai) ([1](https://www.renaissancephilanthropy.org/insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research), [2](https://lean-lang.org/fro/about/)) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) |
-| [Rocq](https://rocq-prover.org/) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/rocq-prover/rocq/commit/3006a6d65)) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) |
+| [Lean](https://leanprover-community.github.io/) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/leanprover/lean4/tree/master/.claude), [2](https://github.com/leanprover/lean4/pull/12776)) <br /> [![AI sponsored](./badges/ai-sponsored-blue.svg)](#sponsored-by-ai) ([1](https://www.renaissancephilanthropy.org/insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research), [2](https://lean-lang.org/fro/about/)) | See below |
+| [Rocq](https://rocq-prover.org/) | [![Request for Help](./badges/request-for-help.svg)](#request-for-help) | [![Permissive AI policy](./badges/permissive-ai-policy-orange.svg)](#permissive-ai-policy) ([1](https://github.com/rocq-prover/rocq/commit/3006a6d65)) | See below |
+
+> [!NOTE]
+> ### Proof Assistants Alternatives
+>
+> * [GNU Aris](https://www.gnu.org/software/aris/)
+> * [metamath](https://us.metamath.org/index.html#downloads): Last release was in 2016.
 
 ## Remote Desktop