|
|
|
|
|
|
by Blaisorblade0
1777 days ago
|
|
|
Do you have a link? That might mean a set of different things, ranging from very hard to impossible; strictly speaking, this seems to go against Godel's theorems tho there are standard workarounds. I'm familiar with https://coq.discourse.group/t/alpha-announcement-coq-is-a-le..., which was just hard, but it does not prove Lean consistent, it only lets Coq process the Lean stdlib. |
|
|