Comment by 7373737373

According to [0], "Rocq’s kernel spans approximately 41K lines of OCaml code, while Lean’s kernel consists of approximately 8K lines of C++ code."

[0] https://dl.acm.org/doi/pdf/10.1145/3747511

My favorite minimalistic example of the Metamath base language (which higher level languages can compile down to), which, saved as, say, prop.mm can be verified with the verifier:

  $c  wff  $.        $( we use this $constant as a type of formula (well formed formula) $)
  $c  ( ) ! ->  $.   $( brackets, negation, implication $)

  $v  A B C  $.      $( $variables to be used in formulas $)

  wa  $f  wff A  $.  $( $floating hypothesis "wa" which says, that A is a well-formed formula $)
  wb  $f  wff B  $.
  wc  $f  wff C  $.

  $( The following assertions define the rules to create formulas $)
  $( In Metamath (unlike Metamath Zero), definitions also use the $axiom statement type $)
  wng  $a wff ! A $.           $( "not A is a well-formed-formula" - mandatory hypotheses are (wa) $)
  wim  $a wff ( A -> B ) $.    $( "A implies B is a well-formed-formula" - mandatory hypotheses are (wa, wb) $)

  $c  |-  $.         $( this $constant will be used as a type of provable formula  $)

  $( Schemes of $axioms of propositional logic $)
  a1  $a |- ( A -> ( B -> A ) ) $.
  a2  $a |- (    ( A -> ( B -> C ) )   ->    ( ( A -> B ) -> ( A -> C ) )    ) $.
  a3  $a |- ( ( ! A -> ! B )  ->  ( B -> A ) ) $.  

  $( Definition of the Modus Ponens rule of inference in new scope; otherwise $essential hypotheses (inputs) mp1, mp2 will become mandatory for all upcoming assertions $)
  ${
      mp1 $e |- A $.                
      mp2 $e |- ( A -> B ) $.
      mp  $a |- B $.               $( mandatory hypotheses of "mp" are (wa, wb, mp1, mp2) $)
  $}

  $( A $proof states the string of symbols to be proven, followed by a list of labels used by the stack machine $)
  $( $floating and $essential hypotheses are pushed onto the top of the stack, $axioms and $proofs transform it by using the top of the stack as inputs $)
  $( When the stack is empty at the end, the proof is successful, and the proved statement can be reused in further proofs using its label $)

  $( " A implies ( B implies C) is a well-formed-formula" $)
  formula1 $p  wff ( A -> ( B -> C ) )  $= wa wb wc wim wim $.

  $( "( A -> A ) -> ( A -> A ) is true (follows from the axioms)" $)
  formula2 $p  |- ( ( A -> A ) -> ( A -> A ) )  $= wa wa wa wim wim    
                                                   wa wa wim wa wa wim  wim  
                                                   wa wa a1    
                                                   wa wa wa a2    
                                                   mp  $.