1. Куча / Говнокод #27829

    0

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 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))
)

    https://mathtoys.org/equations.html
    Доказательство неразрешимости системы уравнений
    x-y=3
    y=5=x
    Где x и y это ℝ
    https://i.imgur.com/oY4FXTN.png

    Запостил: j123123, 17 Ноября 2021

    Комментарии (53) RSS

    • ava j123123 17.11.2021 16:08 # 0

      По-сути это какое-то символьное вычисление вручную, работающее через переписывание. А "Coq" умеет таким вот образом подсказывать вореанты шагов при доказывании питушни своей? Кстати, как это будет доказываться в "Coq"?
      Ответить

      • ava bormand 17.11.2021 16:49 # 0

        > как это будет доказываться в coq

        Вангую, что Proof. lia. Qed. Вечером проверю.

        З.Ы. Хотя тут R...
        Ответить

      • ava bormand 17.11.2021 20:24 # 0

        > Кстати, как это будет доказываться в "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.
        Ответить

        • ava j123123 17.11.2021 22:39 # 0

          И как быстро это работает? Например, квадратную СЛАУ из 10 уравнений оно за сколько решает? Как время решений зависит от размера СЛАУ (какая асимптотическая сложность)? И как оно вообще считает, оно там детерминант ищет(метод Крамера), или что вообще? Сами шаги можешь показать?
          Ответить

          • ava bormand 17.11.2021 22:56 # −1

            Хрен знает, я сварщица не настоящая. В доке пишут про какие-то "конусы", что бы это не значило...

            > шаги

            Петух -- не обучалка. Обычно ты ему советуешь что дальше делать, а не он тебе. А "шаги" от автосольверов там обычно выглядят как нечитаемые лоу-левл портянки.
            Ответить

            • ava j123123 17.11.2021 23:19 # 0

              > А "шаги" от автосольверов там обычно выглядят как нечитаемые лоу-левл портянки.

              Ну, шаги в Metamath выглядят более-менее вменяемо: http://us.metamath.org/mpeuni/_mmbrows2p2e4.png
              Хотя тут не автосольвер, тут вручную доказывалось. Хотя автосольвер к Metamath прикрутить вполне реально. Туда нейронку прикручивали, вот препринт https://arxiv.org/pdf/2009.03393.pdf
              Они обучили нейронку на датасете из кучи доказательств написанных человеками, и потом этой нейронкой смогли найти даже более короткое доказательство какой-то там теоремы.
              Ответить

              • ava bormand 17.11.2021 23:22 # 0

                > обучили нейронку

                Всё, ма-те-ма-ти-ки больше нинужны?
                Ответить

                • ava j123123 17.11.2021 23:26 # 0

                  Ма-те-ма-ти-ки нужны чтобы генерировать новые интересные датасеты для нейронок

                  Кстати, нейронки в Coq что-нибудь доказывать могут? Там есть тактики с встроенными нейросетями?
                  Ответить

                  • ava Soul_re@ver 17.11.2021 23:27 # 0

                    Осталось научить нейронку генерировать датасеты для других нейронок и мешки с мясом не_нужны.
                    Ответить

                    • ava j123123 17.11.2021 23:33 # 0

                      Мешки с мясом со временем пропатчат себе мозг микросхемками, постепенно заменят себе весь мозг этими микросхемками и сами станут искуственными нейронками (осталось только формально доказать, что если мне все нейроны постепенно заменять на микросхемки, и так со временем весь мозг заменить, то я в процессе этой замены не сдохну http://www.rriai.org.ru/eksperiment-s-protezom-mozga-5.html )
                      Ответить

                  • ava CHayT 18.11.2021 01:34 # 0

                    В sauto из coqhammer нейронок нет, но она доказывает без участия человека прямо дофига всего. В последнем проЭкте почти все нудные леммы у меня доказаны ей. Там ещё более продвинутая тактика hammer есть, её пока не пробовала.
                    Ответить

              • ava Hijikata 18.11.2021 15:12 # 0

                Тактики с непредсказуемым поведением не нужны
                Ответить

                • ava bormand 18.11.2021 15:21 # +1

                  И так сойдёт. В конце-концов FPGA и ASIC'и тоже роутят через рандом, алгоритм отжига и какую-то матерь.

                  Даже кнопка реролла есть в гуйне на случай если с сидом не повезло.
                  Ответить

                  • ava Hijikata 18.11.2021 15:41 # +1

                    Не, я не про автосолверы, там, может, и портянка, но её поведение можно предсказать, а с тактикой, обученной нейронкой, могут могут возникнуть проблемы, если она внезапно из-за присутствия в контексте чего-то лишнего сгенерирует другое доказательство. Т.к. forall P : Prop, x : P, y : P. x = y не во всех моделях является правдой, это может сильно усложнить жизнь.
                    Ответить

                    • ava Hijikata 18.11.2021 15:42 # 0

                      Скорее так, тактики с непредсказуемым поведением не нужны, если требуется не просто что-то доказать, но и как-то использовать доказательство.
                      Ответить

                    • ava j123123 18.11.2021 16:01 # 0

                      > а с тактикой, обученной нейронкой, могут могут возникнуть проблемы, если она внезапно из-за присутствия в контексте чего-то лишнего сгенерирует другое доказательство.

                      Ну так это уже бага в самом условии, а не проблема нейронки. Надо делать без лишнего.
                      Ответить

                      • ava Hijikata 18.11.2021 21:04 # 0

                        Ага, а потом кок шлепнет коком по губам, если каждое применение этой нейронной тактики не будет в отдельной лемме
                        Ответить

                    • ava bormand 18.11.2021 16:33 # +2

                      Ну дык и под FPGA в зависимости от фазы луны получаются разные конфигурации, которые могут иметь разные задержки, глюки на переходных процессах и т.п.

                      Забыл формально описать какие-то констрейнты -- ССЗБ, при следующей конпеляции может с ними не повезти.

                      По-моему и в коке так же -- если на что-то не пофиг, надо это что-то формализовать и доказать, а не надеяться, что раз с текущим пруфом повезло, то и дальше будет норм?
                      Ответить

                  • ava Soul_re@ver 18.11.2021 15:54 # +5

                    > Даже кнопка реролла есть в гуйне на случай если с сидом не повезло.
                    3 раза в день бесплатно, за остальные использования нужно платить кристаллами?
                    Ответить

                • ava CHayT 18.11.2021 23:19 # 0


                  Print my_shitty_lemma.
                  C-w
                  C-y
                  Ответить

          • ava bormand 17.11.2021 23:00 # 0

            > Например, квадратную СЛАУ из 10 уравнений оно за сколько решает?

            Theorem bar: exists x y : R, x - y = 2 /\ x + y = 4.

            Tactic failure: Cannot find witness.

            Походу "решать" системы эта тактика вообще не умеет.
            Ответить

          • ava Hijikata 18.11.2021 15:10 # 0

            Ну так никто же не мешает вручную доказать/написать тактику для конкретного класса систем. В моем текущем проекте 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.
            Ответить

            • ava CHayT 18.11.2021 23:23 # +1

              Люблю ssreflect. Сразу видно, что настоящая ма-те-ма-тика.
              Ответить

      • ava Coq 19.11.2021 00:24 # 0

        Ответить

    • ava j123123 17.11.2021 16:25 # 0

      Вот так выглядит доказательство в более понятном виде
      /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" это хуйня какая-то

      Следовательно, решений нет.
      Ответить

      • ava j123123 17.11.2021 16:29 # 0 

        ⎰тест
⎱юникода

⎧1
⎨2
⎩3

        хуета какая-то. Сколько же всякого говна в юникод поназапихивали
        Ответить

        • ava Soul_re@ver 17.11.2021 16:59 # 0

          При попытке отправить смайлик кучи говна, эксепшен хальтит аппликейшн... Странно.
          Ответить

          • ava guest6 17.11.2021 17:06 # 0

            Потому что не все плейны поддерживаются

            пыхеры-с, что с них взять?
            Ответить

        • ava guest6 17.11.2021 17:09 # 0

          Почему хуета? Работает ведь.
          Ответить

          • ava j123123 17.11.2021 17:14 # 0 

            ⎰вот эта
⎱хуета

            с моими шрифтами выглядит хуево. Между этими двумя половинками скобки есть заметная дыра.
            Ответить

            • ava guest6 17.11.2021 17:15 # 0

              пиши в латексте и попроси страйко поставить MathJax: он рендерит латех прямо в браузере
              Ответить

              • ava MaaKut 17.11.2021 17:16 # 0

                Уняк опять спамит (
                Ответить

              • ava j123123 17.11.2021 17:16 # 0

                Надо это на govnomath.ru тогда делать
                Ответить

              • ava j123123 17.11.2021 17:22 # +1

                Страйкеру настолько похуй, что он даже с осетинским уебком нихуя не делает, какой еще нахуй "MathJax"? Надо будет наверное на govnokod.xyz перекатываться
                Ответить

                • ava guest6 17.11.2021 17:38 # 0

                  > Надо будет наверное на govnokod.xyz перекатываться
                  Только перед этим с "WordPress" переписать
                  Ответить

                  • ava guest6 17.11.2021 17:42 # 0

                    напишите на джанге или фласке/alchemy/postgres/jinja, я контрибьютну

                    или можете фронт на ангуляр2/TS, а бек на чем я выше написал
                    Ответить

                    • ava Desktop 17.11.2021 18:03 # 0

                      Сёма?
                      Ответить

                      • ava guest6 17.11.2021 18:11 # 0

                        можете на C# написать, тоже поиграюсь
                        Ответить

                        • ava guest6 17.11.2021 18:12 # 0

                          Могу на "PHP"+"MySQL". Присоединишься?
                          Ответить

                          • ava guest6 17.11.2021 18:16 # 0

                            Давай на Perl под MS-SQL?

                            Кстати, на перле тоже есть фреймворка: Catalyst называ
                            YouPorn was powered by Catalyst[14] until 2012.[15]
                            Ответить

                            • ava bormand 17.11.2021 18:23 # 0

                              > until 2012

                              А потом перевели на "РНР"?
                              Ответить

                              • ava guest6 17.11.2021 18:29 # 0

                                да
                                http://highscalability.com/blog/2012/4/2/youporn-targeting-200-million-views-a-day-and-beyond.html
                                Ответить

                                • ava bormand 17.11.2021 18:33 # 0

                                  Так вот что означает одна из букв P в "PHP"...
                                  Ответить

                                  • ava guest6 17.11.2021 18:41 # 0

                                    А также буква пэ в ламп.

                                    Кстати, все четыре буквы в LAMP -- говно, и как минимум три из них реально не нужны
                                    Ответить

                • ava Desktop 17.11.2021 18:03 # +5

                  xyz это тот сайт, с которого ГК заспамили бесплатной рекламой Виагры и админ которого без разбору называет людей спамерами и уёбками просто потому что?

                  Я лучше со Стертором посижу
                  Ответить

    • ava HE_OTBE4Au_YE6KY 17.11.2021 17:14 # +1

      Астрологи объявили неделю гостя.
      Ответить

    • ava Vahished 17.11.2021 17:16 # 0

      Vanished
      Ответить

    • ava Vahished 17.11.2021 17:17 # 0

      Vanished
      Ответить

    • ava Vahished 17.11.2021 17:17 # 0

      Vanished
      Ответить

    • ava nPOnOBeDHuK 17.11.2021 18:51 # 0

      Биган, малишоус спирит фром анус!
      Похоже, что предпринимаемые Уняком меры эффективны. На говнокодике выросла активность и появилось много новых говнокодов.
      Ответить

    Добавить комментарий