def
definition
def or abbrev
languageModelAlignmentFraction
show as:
view Lean formalization →
formal statement (Lean)
45def languageModelAlignmentFraction : ℚ := 7/8