-
verbose-lean4 Public
Forked from PatrickMassot/verbose-lean4Natural language tactics to teach mathematics using Lean 4
Lean Apache License 2.0 UpdatedDec 26, 2024 -
lean4web Public
Forked from leanprover-community/lean4webThe Lean 4 web editor
TypeScript Apache License 2.0 UpdatedDec 23, 2024 -
MediationInfoStrasbourg Public
Documents utilisés pour de la vulgarisation informatique, surtout du débranché
-
tag_name_script Public
A simple python script to generate name tags from csv list of participants for conferences/worshops.
Python BSD 2-Clause "Simplified" License UpdatedNov 14, 2024 -
leanprover-community.github.io Public
Forked from leanprover-community/leanprover-community.github.ioHosts the website for mathlib and other Lean community infrastructure.
CSS MIT License UpdatedMar 2, 2024 -
europroofnet.github.io Public
Forked from EuroProofNet/europroofnet.github.ioSources of the EuroProofNet web site.
Ruby UpdatedOct 3, 2023 -
coqhammer Public
Forked from lukaszcz/coqhammerCoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
OCaml Other UpdatedOct 20, 2022 -
area-method Public
Forked from rocq-archive/area-methodThe Chou, Gao and Zhang area method
Coq UpdatedSep 16, 2022 -
ATP Public
Forked from EuroProofNet/ATPRepository of EuroProofNet WG 2 on ATPs
Creative Commons Attribution 4.0 International UpdatedJul 10, 2022 -
Coq_verbose Public
Some tactics to write more readable proofs in Coq
-
PA_a_priori_analysis Public
Accompanying files for the paper "Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis"
-
lean-verbose Public
Forked from PatrickMassot/lean-verboseVery controlled natural language tactics for Lean
Lean Apache License 2.0 UpdatedApr 7, 2022 -
cargo-bot-tangible Public
Forked from Pinguee/cargo-bot-tangibleA purely educational rendition of Cargo-Bot, designed to improve students' understanding of recursion.
JavaScript UpdatedJul 8, 2021 -
GeometricAlgebra Public
Forked from thery/GeometricAlgebraWork based on http://www-sop.inria.fr/marelle/GeometricAlgebra/
Coq UpdatedJan 25, 2021 -
GeoProof2006 Public
Repostitory to store the source of GeoProof for software heritage. GeoProof is not maintained anymore.
OCaml GNU General Public License v2.0 UpdatedDec 7, 2020 -
tptp2coq Public
Forked from lukaszcz/tptp2coqConversion of the FOF TPTP format to Coq files
Haskell UpdatedOct 20, 2020 -
-
coq100 Public
Forked from coq-community/coq-100-theoremsStatement of theorems proven in Coq
HTML UpdatedApr 16, 2019 -
opam-coq-archive Public
Forked from coq/opamArchive for all Coq related OPAM packages organized in various repositories
-
InfoSansOrdi Public
Forked from InfoSansOrdi/InfoSansOrdiWiki principal du projet InfoSansOrdi
TeX UpdatedJun 18, 2018 -
-
www Public
Forked from coq/coq.github.ioSources files of the coq.inria.fr website (static part)
HTML UpdatedAug 11, 2016 -
-