民科為什麼不用 Coq 之類的形式化證明工具？

這樣至少能先讓機器檢查一遍，勉強能自圓其說，豈不是美滋滋？

民科怕不是連文檔都看不懂

以下是隨便搜的一「民科」「論文」開頭，請問怎麼把它「形式化」? 請注意我沒有斷章取義，這是該論文第一章第一段，之前沒有任何定義、解釋。

假設 在無限大的宇宙中任取一點，它所對應的都是0而沒有例外，那麼在這種情況下就無所謂存在與不存在，這將是一種沒有任何物質沒有任何變化的虛無。然而這個世 界如果是0與1摻半，那我們就可以稱0為存在稱1為不存在，相反也無妨。但是，0與1的區別是什麼，假設它們是完全靜止的，相互間也就沒有任何聯繫，那麼 它是0或是1就沒有意義了，因為無論它是0還是1對外界來說都沒有任何區別，外界是什麼對它也沒有任何區別。顯然沒有聯繫，沒有相互的影響也就沒有0與1 的差異，同樣無所謂存在與不存在，而這種聯繫或是相互間的影響就是運動。首先我們必須承認運動是相對的，也就是說運動不是0或者1所特有的，它是存在於0 與1之間由它們所共有的東西，那麼運動具體怎麼表現呢，既然只有0與1兩種單位，那對於它們個體而言顯然沒有任何結構了，所以在這裡的運動也就只能是0走 到1的位置，而1走到0的位置，或者說是1變成0，而0變成1的一種互換，假如這個世界的界線現在就只限制在一個0與一個1上，那對於這兩者而言這種互換 將是唯一的運動形式，也是它們唯一的存在形式。

好多民科本身是基於一個錯的前提條件進行的推導得出的結論，而蘊含關係中錯誤的前件一定能推導出一個正確的結論。。。

所以就是，，，用了也沒用，，，人家錯的又不是證明過程。。。

你就不怕民科給你整個：Axiom wannengdingli: False.

題主，你知不知道好多數學家都用不來這玩意兒，真會用就不是民科了

和現有理論是否相容不是民科要解決的首要問題，Coq對民科根本沒用。

民科的問題在於他/她自己拍腦門做出來的那套東西和實驗結果對不上，或者只在某些情況下能用，根本比不過現有理論。如果民科的那套理論和現有理論產生矛盾o不ok？完全ojbk，只要你那套理論也能解釋人類觀測到的所有現象，演繹得出的結論也能合理的預測到一些東西，還比現有理論簡潔優雅/更具普適性，那你完全有資格叫現有理論給你讓路。

只可惜我還沒聽說過這麼牛逼的民科。