[deadbeef57]

(I'm the Johan Commelin mentioned in the blogpost.) In fact, `lie_group` exists in mathlib, and is defined as follows:

  /-- A Lie group is a group and a smooth manifold at the same time in which
  the multiplication and inverse operations are smooth. -/
  -- See note [Design choices about smooth algebraic structures]
  @[ancestor has_smooth_mul, to_additive]
  class lie_group {𝕜 : Type*} [nontrivially_normed_field 𝕜]
    {H : Type*} [topological_space H]
    {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E] (I : model_with_corners 𝕜 E H)
    (G : Type*) [group G] [topological_space G] [charted_space H G]
    extends has_smooth_mul I G : Prop :=
  (smooth_inv : smooth I I (λ a:G, a⁻¹))

In particular, the output of Lean Chat didn't talk at all about needing a smooth inverse function.

Anyway, I very much agree with you that there are risks here. At the same time, I think this can be an extremely useful tool for new users trying to get started. Because mathlib is approaching 1M lines of code, and a tool like this might help a lot in discovering parts of the library. As you say, it can already be used as some sort of snippet-engine-on-steroids.

[JHonaker]

I figured there would be. It just provides another point that it's not really understanding, and it's not really "extracting the pattern".

I really wish half the effort on generation would be spent on leveraging them for guided exploration. It wouldn't matter if you were provided slightly incorrect suggestions for "likely relevant functions," but even likely correct source code doesn't cut it.

Or even snippet prototyping. Like don't use the generated text directly, provide an interface that I can use to transform the generated code into a snippet that I can save.