Are We Stuck with Lean?

Agreed. In addition I think a big reason why we are discussing formalization so much at the moment is that it has only recently become viable to do large scale formalization of mainstream mathematics, using LLMs. These same LLMs will make it much easier to translate from one language to another and port even larger codebases over.

My prediction would therefore be that the LLMs will let us work more-or-less using standard mathematical prose that then gets to codified to some machine-readable and checkable language, but what the language used by the proof checker actually is will be more of a technical detail. In particular, I suspect people will not care too much about the language used for proofs themselves, which means that we might allow for more boilerplate if it is faster to elaborate/compile, unlike current interactive theorem provers which are meant to ease the work of humans. How the language looks like for the statements of the theorems and definitions is probably more important however, since humans will want still to be able to check that what is being formalized corresponds to what they had in mind.

I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.

https://lipn.info/@mevenlennonbertrand/116997927457012577 , you and they might be jumping to conclusions

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  $.