Post #2481103
2026-03-10 21:21 UTC
Announce of Groupoid Infinity theorem prover named Christine resembling Coq 8.2 syntax and semantics, written in Elixir for Erlang/OTP with BEAM byte-code extraction.
https://christine.groupoid.space
Replies (1)
-
@5ht@mathstodon.xyz 2026-03-10 21:22
Before This Exercise you MUST write pure CIC theorem prover named Frank in Miranda-like syntax: https://frank.groupoid.space