CGPA › Proof Assistants
๐Ÿ”
Proof Assistants
Discuss Agda, Coq/Rocq, Lean 4, Idris 2, Isabelle/HOL, F*, NuPRL, Twelf, and all things interactive theorem proving. Dependently typed waifus welcome.
847 threads
12,394 posts
203 members
๐Ÿ“Œ Subforum rules: Be constructive. Termination arguments must be well-founded. Galaxy-brained takes about which proof assistant is "objectively best" will be redirected to #off-topic. Corollary: "Lean would make this trivial" is not a valid reply to an Agda thread. Mods: ProverMoe, IsabelleFan99.
Tip: Use [agda], [lean4], [rocq], [idris2] tags in your post titles for filtering.
๐Ÿ“‚ Sub-categories
Lean 4 / Mathlib Rocq (Coq) Agda Idris 2 Isabelle/HOL F* & Low* NuPRL / Twelf ๐Ÿ“š Resources & Tutorials
โœฆ New Thread
๐Ÿ”ฅ Hot thread
๐Ÿ“Œ Sticky
๐Ÿ†• New posts
๐Ÿ”’ Locked
๐Ÿ“Š Poll
Thread Title Replies Views Last Post
๐Ÿ“Œ Announcements & Stickies
๐Ÿ“Œ Sticky READ BEFORE POSTING: Subforum rules, tagging guide, and resource megathread
by ProverMoe · started 2022-11-01
 12 9,841 CoqGirl 3 weeks ago
๐Ÿ“Œ Sticky [MEGA] "Which proof assistant should I learn?" โ€” Consolidated opinions & flowchart
by IsabelleFan99 · started 2023-03-14 · pages: 1 2 3
248 41,220 dependentcat 2 days ago
๐Ÿ”ฅ Hot & Active Threads
๐Ÿ”ฅ HOT Lean 4 vs. Rocq: the cultural chasm โ€” which side are you on? (2025 edition)
by mathlib_enjoyer · started 6 days ago · pages: 1 2 3 4 5
412 18,774 rocq-chan 4 min ago
๐Ÿ”ฅ HOT NEW Agda 2.7.0 release thread โ€” Mimer replaces Agsy, new instance search, versioning changes
by CubicalCatgirl · started 4 days ago · pages: 1 2
87 5,312 agdanyan 18 min ago
๐Ÿ”ฅ HOT Is Idris 2 actually usable now? Be honest
by lin_redundant · started 9 days ago · pages: 1 2 3
193 11,038 ErasureMode 1 hr ago
๐Ÿ†• NEW Isabelle/HOL appreciation thread โ€” the sleeper pick that verifies seL4 and nobody talks about
by IsabelleFan99 · started 2 days ago
64 3,891 hol_holic 35 min ago
๐Ÿ’ฌ Recent Threads
๐Ÿ†• NEW [rocq] Coq is now officially Rocq โ€” one year later, how do you feel about the rename?
by rocq-chan · started 3 days ago
 51 2,770 ProverMoe 2 hrs ago
๐Ÿ†• SOLVED [agda] Getting Mimer to fill holes in mutual recursion โ€” anyone have tips?
by agdanyan · started 5 days ago
 23 1,204 CubicalCatgirl 6 hrs ago
๐Ÿ’ฌ POLL ๐Ÿ“Š POLL: What is your primary proof assistant in 2025?
by dependentcat · started 1 week ago
 78 7,455 lin_redundant 8 hrs ago
๐Ÿ’ฌ [lean4] Mathlib build times are still insane โ€” is anyone else waiting 45 minutes on a fresh checkout?
by mathlib_enjoyer · started 1 week ago
 34 2,109 lakebuilder 10 hrs ago
๐Ÿ’ฌ SOLVED [f*] F* + Low* workflow setup in 2025 โ€” getting kremlin to cooperate
by kremlin_kitty · started 10 days ago
 17 988 fstar_enjoyer 1 day ago
๐Ÿ’ฌ [nuprl] Is NuPRL still maintained? Asking for a constructivist catgirl
by intuitionist_nya · started 12 days ago
 29 1,637 hol_holic 2 days ago
๐Ÿ’ฌ [twelf] Twelf for logical frameworks โ€” anyone still using it or has Beluga taken over?
by LFProver · started 2 weeks ago
 14 743 LFProver 3 days ago
๐Ÿ’ฌ [idris2] Using linear types in Idris 2 for resource-safe I/O โ€” show your examples
by ErasureMode · started 2 weeks ago
 31 2,018 lin_redundant 4 days ago
๐Ÿ’ฌ [agda] Cubical Agda and univalence in practice โ€” how painful is it really?
by CubicalCatgirl · started 3 weeks ago · pages: 1 2
66 4,512 hottie_prover 5 days ago
๐Ÿ’ฌ SOLVED [rocq] When to use omega vs lia vs ring? Tactic selection guide
by rocq-chan · started 3 weeks ago
 19 3,201 CoqGirl 1 week ago
๐Ÿ’ฌ [lean4] Classical vs. constructive in Lean 4 โ€” Mathlib's classical axioms and what you give up
by intuitionist_nya · started 1 month ago · pages: 1 2
94 5,887 mathlib_enjoyer 1 week ago
๐Ÿ’ฌ [isabelle] Sledgehammer tips & tricks โ€” making it find proofs Isabelle refuses to auto-solve
by hol_holic · started 1 month ago
 42 3,044 IsabelleFan99 1 week ago
๐Ÿ’ฌ [f*] F* for program verification vs Lean 4 โ€” which should I use for verified crypto code?
by kremlin_kitty · started 1 month ago
 38 2,655 fstar_enjoyer 2 weeks ago
๐Ÿ”’ LOCKED [LOCKED] Proof assistant waifu wars: ranking ITP-chans by how much they hate you
by dependentcat · locked by ProverMoe · 6 weeks ago
 312 22,100 ProverMoe 6 weeks ago
๐Ÿ’ฌ [agda] Migrating from agda-stdlib 1.x to 2.x โ€” the breaking change survival guide
by agdanyan · started 2 months ago · pages: 1 2
57 4,221 CubicalCatgirl 3 weeks ago
๐Ÿ’ฌ [idris2] Idris 2 backends compared: Chez Scheme vs Node vs RefC โ€” which is fastest?
by ErasureMode · started 2 months ago
 26 1,789 ErasureMode 1 month ago
โœฆ New Thread
Moderators: ProverMoe, IsabelleFan99  |  Forum tools: RSS Feed · Mark all read · Subscribe to forum
Users browsing this forum: nyanprover, agdanyan, CubicalCatgirl, rocq-chan, and 14 guests  |  18 users online in this subforum right now