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

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

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

        З.Ы. Хотя тут R...
        Ответить
      • > Кстати, как это будет доказываться в "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
              Они обучили нейронку на датасете из кучи доказательств написанных человеками, и потом этой нейронкой смогли найти даже более короткое доказательство какой-то там теоремы.
              Ответить
              • > обучили нейронку

                Всё, ма-те-ма-ти-ки больше нинужны?
                Ответить
                • Ма-те-ма-ти-ки нужны чтобы генерировать новые интересные датасеты для нейронок

                  Кстати, нейронки в Coq что-нибудь доказывать могут? Там есть тактики с встроенными нейросетями?
                  Ответить
                  • Осталось научить нейронку генерировать датасеты для других нейронок и мешки с мясом не_нужны.
                    Ответить
                    • Мешки с мясом со временем пропатчат себе мозг микросхемками, постепенно заменят себе весь мозг этими микросхемками и сами станут искуственными нейронками (осталось только формально доказать, что если мне все нейроны постепенно заменять на микросхемки, и так со временем весь мозг заменить, то я в процессе этой замены не сдохну http://www.rriai.org.ru/eksperiment-s-protezom-mozga-5.html )
                      Ответить
                  • В sauto из coqhammer нейронок нет, но она доказывает без участия человека прямо дофига всего. В последнем проЭкте почти все нудные леммы у меня доказаны ей. Там ещё более продвинутая тактика hammer есть, её пока не пробовала.
                    Ответить
              • Тактики с непредсказуемым поведением не нужны
                Ответить
                • И так сойдёт. В конце-концов FPGA и ASIC'и тоже роутят через рандом, алгоритм отжига и какую-то матерь.

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

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

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

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

                • Print my_shitty_lemma.
                  C-w
                  C-y
                  Ответить
          • > Например, квадратную СЛАУ из 10 уравнений оно за сколько решает?

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

            Tactic failure: Cannot find witness.

            Походу "решать" системы эта тактика вообще не умеет.
            Ответить
          • Ну так никто же не мешает вручную доказать/написать тактику для конкретного класса систем. В моем текущем проекте 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.
            Ответить
            • Люблю ssreflect. Сразу видно, что настоящая ма-те-ма-тика.
              Ответить
      • Ответить
    • Вот так выглядит доказательство в более понятном виде
      /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" это хуйня какая-то

      Следовательно, решений нет.
      Ответить
      • ⎰тест
        ⎱юникода
        
        ⎧1
        ⎨2
        ⎩3

        хуета какая-то. Сколько же всякого говна в юникод поназапихивали
        Ответить
        • При попытке отправить смайлик кучи говна, эксепшен хальтит аппликейшн... Странно.
          Ответить
          • Потому что не все плейны поддерживаются

            пыхеры-с, что с них взять?
            Ответить
        • Почему хуета? Работает ведь.
          Ответить
          • ⎰вот эта
            ⎱хуета

            с моими шрифтами выглядит хуево. Между этими двумя половинками скобки есть заметная дыра.
            Ответить
            • пиши в латексте и попроси страйко поставить MathJax: он рендерит латех прямо в браузере
              Ответить
              • Уняк опять спамит (
                Ответить
              • Надо это на govnomath.ru тогда делать
                Ответить
              • Страйкеру настолько похуй, что он даже с осетинским уебком нихуя не делает, какой еще нахуй "MathJax"? Надо будет наверное на govnokod.xyz перекатываться
                Ответить
                • > Надо будет наверное на govnokod.xyz перекатываться
                  Только перед этим с "WordPress" переписать
                  Ответить
                  • напишите на джанге или фласке/alchemy/postgres/jinja, я контрибьютну

                    или можете фронт на ангуляр2/TS, а бек на чем я выше написал
                    Ответить
                    • Сёма?
                      Ответить
                      • можете на C# написать, тоже поиграюсь
                        Ответить
                        • Могу на "PHP"+"MySQL". Присоединишься?
                          Ответить
                          • Давай на Perl под MS-SQL?

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

                              А потом перевели на "РНР"?
                              Ответить
                              • да
                                http://highscalability.com/blog/2012/4/2/youporn-targeting-200-million-views-a-day-and-beyond.html
                                Ответить
                                • Так вот что означает одна из букв P в "PHP"...
                                  Ответить
                                  • А также буква пэ в ламп.

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

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

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