Constant MATH_INCOMPLETENESS_LITERATE 

pub const MATH_INCOMPLETENESS_LITERATE: &str = r###"-- ============================================
-- GÖDEL'S FIRST INCOMPLETENESS THEOREM (Literate Mode)
-- ============================================
-- "If LOGOS is consistent, then G is not provable"
--
-- This example demonstrates fully Literate syntax:
-- - "## To be Predicate" for predicate definitions
-- - "## To be Consistent -> Prop:" for nullary predicates
-- - "## Theorem:" blocks with "Statement:"
-- - "X implies Y" for logical implication
-- - "X equals Y" for equality propositions

-- ============================================
-- 1. THE PROVABILITY PREDICATE
-- ============================================

## To be Provable (s: Syntax) -> Prop:
    Yield there exists a d: Derivation such that (concludes(d) equals s).

-- ============================================
-- 2. CONSISTENCY DEFINITION
-- ============================================
-- A system is consistent if it cannot prove False

Let False_Name be the Name "False".

## To be Consistent -> Prop:
    Yield Not(Provable(False_Name)).

-- ============================================
-- 3. THE GÖDEL SENTENCES
-- ============================================

Let T be Apply(the Name "Not", Apply(the Name "Provable", Variable 0)).
Let G be the diagonalization of T.

-- ============================================
-- 4. THE THEOREM STATEMENT
-- ============================================

## Theorem: Godel_First_Incompleteness
    Statement: Consistent implies Not(Provable(G)).

-- ============================================
-- VERIFICATION
-- ============================================

Check Godel_First_Incompleteness.
Check Consistent.
Check Provable(G).
Check Not(Provable(G)).
"###;