Add mrmartin/On-Formally-Undecidable-Propositions-of-NP

[Copilot]

Adds mrmartin/On-Formally-Undecidable-Propositions-of-NP — a Lean 4 formalization accompanying the paper "On Formally Undecidable Propositions of Nondeterministic Complexity and Related Classes", proving the impossibility of a complete Hilbert triple for arithmetic, Gödel's incompleteness theorems, and regeneration of independence under theory extension.

Changes

• ALF/Authors.lean — New author entry: mrmartin (Martin Kolar)
• ALF/Bibliography.lean — New repository entry tagged arithmetic + incompleteness_theorem, added to the bibliography list

def «mrmartin/On-Formally-Undecidable-Propositions-of-NP» : Repository where
  url := .mk "mrmartin" "On-Formally-Undecidable-Propositions-of-NP"
  tp := [.Lean4]
  authors := [«mrmartin»]
  tags := [.arithmetic, .incompleteness_theorem]
  description := "Machine-checked Lean 4 proof ..."