remote/open-slopware
1
0
Fork 0
mirror of https://codeberg.org/small-hack/open-slopware.git synced 2026-10-15 05:47:07 +02:00
Code Issues Projects Releases Packages Wiki Activity

add proof-assistant alternatives (#1718)

Browse source 
### Description of Changes

Alternatives: add GNU Aris, metamath
Co-authored-by: ethical-foss-admin <ethical-foss-admin@noreply.codeberg.org>
Reviewed-on: https://codeberg.org/ethical-foss/open-slopware/pulls/1718
Reviewed-by: Ethical FOSS admin <ethical-foss-admin@noreply.codeberg.org>
This commit is contained in:
Allen123456hello 2026-10-07 09:50:21 +02:00 • committed by Allen
commit ce2c04b969
1 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

13
README.md
View file

@ -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