Нашли или выдавили из себя код, который нельзя назвать нормальным,
на который без улыбки не взглянешь?
Не торопитесь его удалять или рефакторить, — запостите его на
говнокод.ру, посмеёмся вместе!
По-сути это какое-то символьное вычисление вручную, работающее через переписывание. А "Coq" умеет таким вот образом подсказывать вореанты шагов при доказывании питушни своей? Кстати, как это будет доказываться в "Coq"?
Require Import Coq.Reals.Reals.
Require Import Lra.
Open Scope R_scope.
Theorem foo:
forall x y : R, x - y = 3 /\ y + 5 = x -> False.
Proof.
intros. lra.
Qed.
И как быстро это работает? Например, квадратную СЛАУ из 10 уравнений оно за сколько решает? Как время решений зависит от размера СЛАУ (какая асимптотическая сложность)? И как оно вообще считает, оно там детерминант ищет(метод Крамера), или что вообще? Сами шаги можешь показать?
Хрен знает, я сварщица не настоящая. В доке пишут про какие-то "конусы", что бы это не значило...
> шаги
Петух -- не обучалка. Обычно ты ему советуешь что дальше делать, а не он тебе. А "шаги" от автосольверов там обычно выглядят как нечитаемые лоу-левл портянки.
> А "шаги" от автосольверов там обычно выглядят как нечитаемые лоу-левл портянки.
Ну, шаги в Metamath выглядят более-менее вменяемо: http://us.metamath.org/mpeuni/_mmbrows2p2e4.png
Хотя тут не автосольвер, тут вручную доказывалось. Хотя автосольвер к Metamath прикрутить вполне реально. Туда нейронку прикручивали, вот препринт https://arxiv.org/pdf/2009.03393.pdf
Они обучили нейронку на датасете из кучи доказательств написанных человеками, и потом этой нейронкой смогли найти даже более короткое доказательство какой-то там теоремы.
Мешки с мясом со временем пропатчат себе мозг микросхемками, постепенно заменят себе весь мозг этими микросхемками и сами станут искуственными нейронками (осталось только формально доказать, что если мне все нейроны постепенно заменять на микросхемки, и так со временем весь мозг заменить, то я в процессе этой замены не сдохну http://www.rriai.org.ru/eksperiment-s-protezom-mozga-5.html )
В sauto из coqhammer нейронок нет, но она доказывает без участия человека прямо дофига всего. В последнем проЭкте почти все нудные леммы у меня доказаны ей. Там ещё более продвинутая тактика hammer есть, её пока не пробовала.
Не, я не про автосолверы, там, может, и портянка, но её поведение можно предсказать, а с тактикой, обученной нейронкой, могут могут возникнуть проблемы, если она внезапно из-за присутствия в контексте чего-то лишнего сгенерирует другое доказательство. Т.к. forall P : Prop, x : P, y : P. x = y не во всех моделях является правдой, это может сильно усложнить жизнь.
> а с тактикой, обученной нейронкой, могут могут возникнуть проблемы, если она внезапно из-за присутствия в контексте чего-то лишнего сгенерирует другое доказательство.
Ну так это уже бага в самом условии, а не проблема нейронки. Надо делать без лишнего.
Ну дык и под FPGA в зависимости от фазы луны получаются разные конфигурации, которые могут иметь разные задержки, глюки на переходных процессах и т.п.
Забыл формально описать какие-то констрейнты -- ССЗБ, при следующей конпеляции может с ними не повезти.
По-моему и в коке так же -- если на что-то не пофиг, надо это что-то формализовать и доказать, а не надеяться, что раз с текущим пруфом повезло, то и дальше будет норм?
Ну так никто же не мешает вручную доказать/написать тактику для конкретного класса систем. В моем текущем проекте set_solver вызывается часто для определенных целей, поэтому у меня есть стремительный my_set_solver.
Require Import Coq.Reals.Reals.
Require Import ssreflect.
Open Scope R_scope.
Theorem foo:
forall x y : R, x - y = 3 /\ y + 5 = x -> False.
Proof.
move=> x y; elim=> p q; rewrite -q /Rminus Rplus_comm -Rplus_assoc (Rplus_comm _ y) Rplus_opp_r Rplus_0_l in p.
by apply eq_IZR in p.
Qed.
Вот так выглядит доказательство в более понятном виде
/x-y=3
\y+5=x
/x=3+y // тут переносим y влево
\x=y+5 // тут разворачиваем
/y+5=y+3 // подставляем вместо "x" выражение "y+5"
\x=y+5
/5=3 // убираем слева и справа "y"
\x=y+5
5=3 ≡ 5-3=0 ≡ 2=0
"2=0" это хуйня какая-то
Страйкеру настолько похуй, что он даже с осетинским уебком нихуя не делает, какой еще нахуй "MathJax"? Надо будет наверное на govnokod.xyz перекатываться
xyz это тот сайт, с которого ГК заспамили бесплатной рекламой Виагры и админ которого без разбору называет людей спамерами и уёбками просто потому что?
Биган, малишоус спирит фром анус! Похоже, что предпринимаемые Уняком меры эффективны. На говнокодике выросла активность и появилось много новых говнокодов.
j123123 # 0
bormand # 0 ⇈
Вангую, что Proof. lia. Qed. Вечером проверю.
З.Ы. Хотя тут R...
bormand # 0 ⇈
j123123 # 0 ⇈
bormand # 0 ⇈
> шаги
Петух -- не обучалка. Обычно ты ему советуешь что дальше делать, а не он тебе. А "шаги" от автосольверов там обычно выглядят как нечитаемые лоу-левл портянки.
j123123 # 0 ⇈
Ну, шаги в Metamath выглядят более-менее вменяемо: http://us.metamath.org/mpeuni/_mmbrows2p2e4.png
Хотя тут не автосольвер, тут вручную доказывалось. Хотя автосольвер к Metamath прикрутить вполне реально. Туда нейронку прикручивали, вот препринт https://arxiv.org/pdf/2009.03393.pdf
Они обучили нейронку на датасете из кучи доказательств написанных человеками, и потом этой нейронкой смогли найти даже более короткое доказательство какой-то там теоремы.
bormand # 0 ⇈
Всё, ма-те-ма-ти-ки больше нинужны?
j123123 # 0 ⇈
Кстати, нейронки в Coq что-нибудь доказывать могут? Там есть тактики с встроенными нейросетями?
[email protected] # 0 ⇈
j123123 # 0 ⇈
CHayT # 0 ⇈
Hijikata # 0 ⇈
bormand # 0 ⇈
Даже кнопка реролла есть в гуйне на случай если с сидом не повезло.
Hijikata # 0 ⇈
Hijikata # 0 ⇈
j123123 # 0 ⇈
Ну так это уже бага в самом условии, а не проблема нейронки. Надо делать без лишнего.
Hijikata # 0 ⇈
bormand # 0 ⇈
Забыл формально описать какие-то констрейнты -- ССЗБ, при следующей конпеляции может с ними не повезти.
По-моему и в коке так же -- если на что-то не пофиг, надо это что-то формализовать и доказать, а не надеяться, что раз с текущим пруфом повезло, то и дальше будет норм?
[email protected] # 0 ⇈
3 раза в день бесплатно, за остальные использования нужно платить кристаллами?
CHayT # 0 ⇈
Print my_shitty_lemma.
C-w
C-y
bormand # 0 ⇈
Theorem bar: exists x y : R, x - y = 2 /\ x + y = 4.
Tactic failure: Cannot find witness.
Походу "решать" системы эта тактика вообще не умеет.
[email protected] # 0 ⇈
Убрали всех свидетелей?
Hijikata # 0 ⇈
CHayT # 0 ⇈
Coq # 0 ⇈
j123123 # 0
Следовательно, решений нет.
j123123 # 0 ⇈
хуета какая-то. Сколько же всякого говна в юникод поназапихивали
[email protected] # 0 ⇈
guest # 0 ⇈
пыхеры-с, что с них взять?
guest # 0 ⇈
j123123 # 0 ⇈
с моими шрифтами выглядит хуево. Между этими двумя половинками скобки есть заметная дыра.
guest # 0 ⇈
MaaKut # 0 ⇈
j123123 # 0 ⇈
j123123 # 0 ⇈
guest # 0 ⇈
Только перед этим с "WordPress" переписать
guest # 0 ⇈
или можете фронт на ангуляр2/TS, а бек на чем я выше написал
Desktop # 0 ⇈
guest # 0 ⇈
guest # 0 ⇈
guest # 0 ⇈
Кстати, на перле тоже есть фреймворка: Catalyst называ
YouPorn was powered by Catalyst[14] until 2012.[15]
bormand # 0 ⇈
А потом перевели на "РНР"?
guest # 0 ⇈
http://highscalability.com/blog/2012/4/2/youporn-targeting-200-million-views-a-day-and-beyond.html
bormand # 0 ⇈
guest # 0 ⇈
Кстати, все четыре буквы в LAMP -- говно, и как минимум три из них реально не нужны
ObeseYoung # 0 ⇈
Desktop # 0 ⇈
Я лучше со Стертором посижу
guest # 0 ⇈
HE_OTBE4Au_YE6KY # 0
Vahished # 0
Vahished # 0
Vahished # 0
nPOnOBeDHuK # 0
Похоже, что предпринимаемые Уняком меры эффективны. На говнокодике выросла активность и появилось много новых говнокодов.