Timeline for Formalization of a model of ∞-category in a proof assistant
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 3, 2023 at 10:32 | answer | added | Maximilian Doré | timeline score: 2 | |
| Sep 16, 2023 at 9:09 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 46 characters in body
|
| Aug 15, 2023 at 7:19 | answer | added | Alex Chichigin | timeline score: 2 | |
| Aug 12, 2023 at 17:58 | comment | added | TomR | Indeed authors of the referenced paper is doing formalization themselves in rzk. I am checking how much this can be integrated with vast libraries of Coq or some other provers. | |
| Aug 12, 2023 at 17:19 | comment | added | Trebor♦ | Since you talk about synthetic inf-category theory, do you know that it is implemented in the proof assistant rzk? | |
| Aug 12, 2023 at 3:32 | history | edited | TomR | CC BY-SA 4.0 |
added 883 characters in body
|
| Aug 11, 2023 at 19:51 | comment | added | Ronald J. Zallman | Mathlib does not appear to have the Whitehead theorem. | |
| Aug 11, 2023 at 19:49 | comment | added | Ronald J. Zallman | Agda has a lot of cubical type theory going on. | |
| Aug 11, 2023 at 14:12 | comment | added | Trebor♦ | Agda doesn't have a trusted core, in fact homotopy.io probably has fewer bugs than agda. But if what you want is that level of trustworthiness it is fine, and you should probably include that in your question. | |
| Aug 11, 2023 at 11:50 | comment | added | TomR | And isolated calculi are not part of formal math library which can be encoded in large language model in its entirety and whose one part can be used for suggestions how to generate new proofs or theorems in other parts. | |
| Aug 11, 2023 at 11:46 | comment | added | TomR | No, I just assumed: if homotopy.io is written in Javascript, then it is kind of Wolfram Alpha - just implementation of some calculus. The situation with proof assistants is different - every piece of code and its execution can be traced up to trusted core. I am not sure if Javascript and its on-the-fly compiler and its VM has such formal proof up to some trusted core. Calculi are great, but sometimes they are not formalization. | |
| Aug 11, 2023 at 11:33 | comment | added | Trebor♦ | I don't quite understand the javascript part. Does rewriting, say, agda using javascript (it is currently written in haskell) discredit its results somehow? | |
| S Aug 11, 2023 at 11:01 | review | First questions | |||
| Aug 13, 2023 at 12:29 | |||||
| S Aug 11, 2023 at 11:01 | history | asked | TomR | CC BY-SA 4.0 |