The future of interactive theorem proving?
I want to preface this by saying I&#x27;m not trying to hate on the author. Good on them for applying a new technology to try to solve an annoying part of their work. I hope they continue to be creative and fearless in their approach to problem solving. The comments that follow are born more out of my increasing frustration with the ML and ML-adjacent communities that seem to have failed to learn anything about the dangers of hype and over-promising from the 1980s (and really just human history in general).<p>While it&#x27;s an undeniable achievement that these kinds of models can generate syntactically correct code or even the correct solution <i>some of the time</i>. I find it hard to get excited about them for anything but boilerplate (and even they I think they pose the greatest risk, lulling one into a false sense of security until you get bitten).<p>If we take formal methods as the way to ensure the code we&#x27;ve written provably does what we say it does, we had better damn well make sure that what we&#x27;ve said it does is what we want it to do. In other words, I feel like this is offloading the most important part of the problem, and the one that <i>can&#x27;t</i> be checked automatically onto a very iffy situation.<p>We should really stop to consider what these kinds of models are. Pattern recognizers, not thinking machines. See the author&#x27;s quote about this theorem:<p><pre><code>    Let G be a Lie group. Then the tangent space at the identity is a Lie algebra.
</code></pre>
which is translated into the theorem:<p><pre><code>    theorem tangent_space_at_identity_is_lie_algebra (G : Type*) [group G]
      [topological_space G] [topological_group G] [charted_space G] [smooth_manifold G] :
        lie_algebra (tangent_space_at_identity G) :=
</code></pre>
Their quote<p><pre><code>    For some completely unclear reason, the app decides to consider a Lie algebra over \mathbb{R} instead of my explicit instruction to use a field k, and that’s even before addressing the fact that tangent_space_at_identity is not a mathlib definition. I tried a few different responses to the app’s initial attempt, and couldn’t get it to do anything helpful.
</code></pre>
They try to fix this by &quot;prompt engineering&quot;:<p><pre><code>    You must specify a field for your Lie algebra as in lie_algebra k M
</code></pre>
which leads to the change:<p><pre><code>    lie_algebra R (tangent_space_at_identity G) :=
</code></pre>
This is exactly the kind of boilerplate we&#x27;d want to automate with this. The specification of a Lie group seems onerous here, but it&#x27;s also exactly the kind of mistake that makes using this kind of mistake that makes relying on these systems so scary. Here it&#x27;s a syntax pattern, and we have to end up proving the correctness, so maybe we wouldn&#x27;t notice the mistake here. It&#x27;s almost certainly going to be missed often in (choose your favorite dynamically typed interpreted language that let&#x27;s you find all this fun stuff out at runtime). There is no understanding of what we do and do not know. What we&#x27;ve proved or have yet to prove be damned.<p>I guess my point hinges completely on what you consider &quot;knowing&quot; to be. It&#x27;s kind of funny. Nobody would ever say that a compiler knows how to transform one language to another. The personification of ML really irks me. I try very hard to avoid it, but it&#x27;s easy to slip.<p>I don&#x27;t want to say we should throw the baby out with the bathwater. I do think that there are uses for these things. The recognition of the pattern for the syntax to specify the characteristics of a Lie group would make a great first pass at a snippet template. (This is ignoring the question of why isn&#x27;t Lie_group a definition that just pulls in the necessary requirements on G rather than needing to specify them each time. If one of those is not really a requirement for Lie groups, forgive me, my exposure to Lie theory is very limited.)<p>I would be much more interested in a tool that allows me to identify patterns in the code with a summary printout or something like the likelihood of a given pattern in the neighborhood of my cursor. The generation part is just not good enough to trust IMO.<p>Also, I really hope we see some sort of backlash for MS just deciding to just ignore everyone&#x27;s&#x27; licenses.