Hello,
Have any of you tried the proof assistants (lean, coq etc)? Is it applicable to the problems of the site?
thank you
→ Обратите внимание
→ Лидеры (рейтинг)
| № | Пользователь | Рейтинг |
|---|---|---|
| 1 | Benq | 3676 |
| 2 | Kevin114514 | 3659 |
| 3 | jiangly | 3640 |
| 4 | turmax | 3450 |
| 5 | tourist | 3408 |
| 6 | strapple | 3360 |
| 7 | Um_nik | 3354 |
| 8 | squareOf105 | 3348 |
| 9 | maroonrk | 3312 |
| 10 | idontwannadothis…e | 3191 |
| Страны | Города | Организации | Всё → |
→ Лидеры (вклад)
| № | Пользователь | Вклад |
|---|---|---|
| 1 | Qingyu | 155 |
| 2 | nik_exists | 151 |
| 3 | maspy | 149 |
| 4 | AmShZ | 145 |
| 5 | Um_nik | 143 |
| 6 | Errichto | 139 |
| 7 | BledDest | 136 |
| 8 | adamant | 135 |
| 9 | maroonrk | 133 |
| 10 | cry | 130 |
→ Найти пользователя
→ Прямой эфир
Codeforces (c) Copyright 2010-2026 Михаил Мирзаянов
Соревнования по программированию 2.0
Время на сервере: 08.11.2026 20:00:26 (g2).
Десктопная версия, переключиться на мобильную.
При поддержке
I actually wrote a short blog, using CP problems as an introduction to Coq. Coq in particular has an extraction mechanism that allows you to prove a function correct according to a specification, and then extract it into a Ocaml/Haskell program you can submit to CF and most judges.
Now doing so in-contest is not really useful/feasible. Also, I don't think proof assistants like Coq or Lean are well-suited for reasoning about imperative programs; there are some languages like Dafny that might be more appropriate for that.
I didn't imagine to use it during a contest ^^ I was going for lean, do you think that coq is more suitable? The coq code is much less readable than lean....
I'm not sure exactly what your goal is, but IMO the two are fairly similar.
It's hard going. But it's worth giving a try. I'm working on CoqCP, a repository of formalized CP proofs. No running programs yet, but there will be some. The repository is still in its early stages. I want the repository to be bigger and cover more CP problems. It would take me a lot of practice to be able to use the technology in contest, but I'm working to get there.