- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
(steps
(1 given (t (((x - y) = 3) & ((y + 5) = x))))
(2 rewrite (s 1) (path "/main/right/right") (t ((x = y) == (y = x))))
(3 addThisToBoth (s 2) (path "/main/right/left/left/right"))
(4 arrangeSum (s 3) (path "/right/right/left/right"))
(5 simplifySite (s 4) (path "/right/right/left/left"))
(6 replaceConjunct (s 5) (path "/right/right/left/left"))
(7 subtractThisFromBoth (s 6) (path "/right/right/left/left/left"))
(8 arrangeSum (s 7) (path "/right/right/left/right"))
(9 simplifySite (s 8) (path "/right/right/left/right"))
(10 arrangeSum (s 9) (path "/right/right/left/left"))
(11 simplifySite (s 10) (path "/right/right/left/left"))
(12 rewrite (s 11) (path "/right/right/left") (t (((R a) & (R b)) => ((a = b) == ((a - b) = 0)))))
(13 simplifyFocalPart (s 12))
(14 modusPonens (s 1) (s 13))
)
j123123 17.11.2021 16:08 # 0
bormand 17.11.2021 16:49 # 0
Вангую, что Proof. lia. Qed. Вечером проверю.
З.Ы. Хотя тут R...
bormand 17.11.2021 20:24 # 0
j123123 17.11.2021 22:39 # 0
bormand 17.11.2021 22:56 # −1
> шаги
Петух -- не обучалка. Обычно ты ему советуешь что дальше делать, а не он тебе. А "шаги" от автосольверов там обычно выглядят как нечитаемые лоу-левл портянки.
j123123 17.11.2021 23:19 # 0
Ну, шаги в Metamath выглядят более-менее вменяемо: http://us.metamath.org/mpeuni/_mmbrows2p2e4.png
Хотя тут не автосольвер, тут вручную доказывалось. Хотя автосольвер к Metamath прикрутить вполне реально. Туда нейронку прикручивали, вот препринт https://arxiv.org/pdf/2009.03393.pdf
Они обучили нейронку на датасете из кучи доказательств написанных человеками, и потом этой нейронкой смогли найти даже более короткое доказательство какой-то там теоремы.
bormand 17.11.2021 23:22 # 0
Всё, ма-те-ма-ти-ки больше нинужны?
j123123 17.11.2021 23:26 # 0
Кстати, нейронки в Coq что-нибудь доказывать могут? Там есть тактики с встроенными нейросетями?
Soul_re@ver 17.11.2021 23:27 # 0
j123123 17.11.2021 23:33 # 0
CHayT 18.11.2021 01:34 # 0
Hijikata 18.11.2021 15:12 # 0
bormand 18.11.2021 15:21 # +1
Даже кнопка реролла есть в гуйне на случай если с сидом не повезло.
Hijikata 18.11.2021 15:41 # +1
Hijikata 18.11.2021 15:42 # 0
j123123 18.11.2021 16:01 # 0
Ну так это уже бага в самом условии, а не проблема нейронки. Надо делать без лишнего.
Hijikata 18.11.2021 21:04 # 0
bormand 18.11.2021 16:33 # +2
Забыл формально описать какие-то констрейнты -- ССЗБ, при следующей конпеляции может с ними не повезти.
По-моему и в коке так же -- если на что-то не пофиг, надо это что-то формализовать и доказать, а не надеяться, что раз с текущим пруфом повезло, то и дальше будет норм?
Soul_re@ver 18.11.2021 15:54 # +5
3 раза в день бесплатно, за остальные использования нужно платить кристаллами?
CHayT 18.11.2021 23:19 # 0
Print my_shitty_lemma.
C-w
C-y
bormand 17.11.2021 23:00 # 0
Theorem bar: exists x y : R, x - y = 2 /\ x + y = 4.
Tactic failure: Cannot find witness.
Походу "решать" системы эта тактика вообще не умеет.
Soul_re@ver 17.11.2021 23:01 # +1
Убрали всех свидетелей?
Hijikata 18.11.2021 15:10 # 0
CHayT 18.11.2021 23:23 # +1
Coq 19.11.2021 00:24 # 0
j123123 17.11.2021 16:25 # 0
Следовательно, решений нет.
j123123 17.11.2021 16:29 # 0
хуета какая-то. Сколько же всякого говна в юникод поназапихивали
Soul_re@ver 17.11.2021 16:59 # 0
guest6 17.11.2021 17:06 # 0
пыхеры-с, что с них взять?
guest6 17.11.2021 17:09 # 0
j123123 17.11.2021 17:14 # 0
с моими шрифтами выглядит хуево. Между этими двумя половинками скобки есть заметная дыра.
guest6 17.11.2021 17:15 # 0
MaaKut 17.11.2021 17:16 # 0
j123123 17.11.2021 17:16 # 0
j123123 17.11.2021 17:22 # +1
guest6 17.11.2021 17:38 # 0
Только перед этим с "WordPress" переписать
guest6 17.11.2021 17:42 # 0
или можете фронт на ангуляр2/TS, а бек на чем я выше написал
Desktop 17.11.2021 18:03 # 0
guest6 17.11.2021 18:11 # 0
guest6 17.11.2021 18:12 # 0
guest6 17.11.2021 18:16 # 0
Кстати, на перле тоже есть фреймворка: Catalyst называ
YouPorn was powered by Catalyst[14] until 2012.[15]
bormand 17.11.2021 18:23 # 0
А потом перевели на "РНР"?
guest6 17.11.2021 18:29 # 0
http://highscalability.com/blog/2012/4/2/youporn-targeting-200-million-views-a-day-and-beyond.html
bormand 17.11.2021 18:33 # 0
guest6 17.11.2021 18:41 # 0
Кстати, все четыре буквы в LAMP -- говно, и как минимум три из них реально не нужны
ObeseYoung 18.11.2021 03:06 # −1
Desktop 17.11.2021 18:03 # +5
Я лучше со Стертором посижу
guest6 17.11.2021 18:04 # 0
HE_OTBE4Au_YE6KY 17.11.2021 17:14 # +1
Vahished 17.11.2021 17:16 # 0
Vahished 17.11.2021 17:17 # 0
Vahished 17.11.2021 17:17 # 0
nPOnOBeDHuK 17.11.2021 18:51 # 0
Похоже, что предпринимаемые Уняком меры эффективны. На говнокодике выросла активность и появилось много новых говнокодов.