Top new questions this week:
|
|
Record types are a common feature in most paradigms. Agda also allows defining records with the coinductive keyword. Lastly there are the seemingly more exotic co(…
|
|
I am considering whether I should learn the ACL2 proof assistant. However, before diving into that, I wanted to know if there are significant limitations in terms of proving math. The first thing I …
|
|
I am trying to prove the following fact while learning the J-Bob language: that any non-negative natural number is positive (with my proof attempts below). The fact seems simple enough. However, I …
|
Greatest hits from previous weeks:
|
|
Impredicativity greatly increases the logical strength of a formal system, and impredicative propositions are also a consequence of various axioms including LEM and Zorn’s Lemma. An impredicative sort …
|
|
Off and on I have heard of the jargon “commuting conversion” but I don’t really know what it means. I’ve heard commuting conversions are problematic but I don’t know why.
|
|
As far as I know, the default configuration for the Lean VSCode plugin checks the code continuously, and so even when the user is in the middle of typing an expression, Lean will immediately report a …
|
|
I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/…
|
|
Every community can have inside jokes among it, and April Fool’s jokes are a common variety, but proof assistants are particularly susceptible to April Fool’s jokes. They have strong guarantees of …
|
|
I am a high school senior going into college and I am applying to a scholarship in which I must write an essay about a potential future technology that would dramatically impact humans. I immediately …
|
|
Higher structures in category theory lead very organically to visual or graphical interpretations in terms of string diagrams and commuting squares. However, it seems hard to implement a graphical …
|
