Куча говна / Говнокод #27829 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  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 j123123, (Updated )

Комментарии (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 раза в день бесплатно, за остальные использования нужно платить кристаллами?
                  Ответить
        • > Например, квадратную СЛАУ из 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: он рендерит латех прямо в браузере
            Ответить
            • Страйкеру настолько похуй, что он даже с осетинским уебком нихуя не делает, какой еще нахуй "MathJax"? Надо будет наверное на govnokod.xyz перекатываться
              Ответить
              • > Надо будет наверное на govnokod.xyz перекатываться
                Только перед этим с "WordPress" переписать
                Ответить
              • xyz это тот сайт, с которого ГК заспамили бесплатной рекламой Виагры и админ которого без разбору называет людей спамерами и уёбками просто потому что?

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

Добавить комментарий для Hijikata Отменить ответ

Помни, guest, за тобой могут следить!

    А не использовать ли нам bbcode?


    8