Undecidable languages are formal languages, too, even though there's no Turing machine that can accurately determine for any string whether it is part of the language or not.

A formal language is a set of finite-length sequences (called "words") of symbols from another set (called the "alphabet"). It's essentially a very crude approximation of some strings of letters in an alphabetic writing system forming words in a natural language, while other combinations are just nonsense.

For a given formal language, there don't necessarily have to be any rules governing the words of the language, though the languages used for writing formal proofs are typically more well-behaved.

Use of the word "mechanical" to describe formal reasoning predates computers.

Here's the first sentence of Godel's 1931 On formally undecidable propositions...

"The development of mathematics in the direction of greater exactness has—as is well known—led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules."

Leibniz had discussed calculating machines (and even thought about binary arithmetic being the most appropriate implementation), so the general idea probably goes back quite far

Edit: Oh, I guess by "late 1930s" you're referring to Turing's 1936 paper where he defines Turing machines, rather than actual electronic computers. Still, understanding "formal" as "mechanical" predates it.

Well said.

Also i highly recommend everybody to read the great logician Alfred Tarski's classic book Introduction to Logic: And to the Methodology of Deductive Sciences to really understand "Logic" which is what Formal Reasoning is based on.

Well, they can't always be correctly interpreted by computers. Computers misinterpret formal languages all the time! And since GPT-2, computers are reasonably frequently able to interpret informal languages correctly too.

> So first let it translate natural language to a formal language, from there allow it to use a logic engine to make verifiable transformations (correctness-preserving), and finally translate back to natural language.

Linguists in the Richard Montague tradition have indeed attempted to use tools like formal logic, lambda calculus, continuations, monads, modalities etc. to try and understand the semantics of natural language in a way that's both logical/formal and compositional - i.e. accounting at least partially for the "deep" syntax of natural language itself, such that a fragment can be said to have a semantics of its own and the global semantics of a broader construction arises from "composing" these narrower semantics in a reasonably straightforward way.

This is pretty much the same as trying to take the "let's translate natural language into formal logic" proof-of-concept exercises from a text like OP (or from your average logic textbook) seriously and extending them to natural language as a whole. It turns out that this is really, really hard, because natural language mixes multiple "modalities" together in what looks like a very ad-hoc way. We only barely have the tools in formal logic to try and replicate this, such as continuations, modalities and monads. (Linguists actually talk about many phenomena of this kind, talking about "modalities" is just one example that's both general enough to give a broad idea and happens to be straightforward enough on the logical side. You have quantification, intensionality, anaphora, scope, presupposition, modality proper, discourse-level inference, pragmatics, ellipsis, indexicals, speech acts, etc. etc. etc.)

And because the semantics of natural language is both so general and so hard to pin down, it doesn't seem useful to "reason" about the logical semantics of natural languages so directly. You can of course use logical/mathematical modeling to address all sorts of problems, but this doesn't occur via a verbatim "translation" from some specific language utterance.

I've been strapping different LLM based setups to Lean 4 with a variety of different prompting methods. My biggest conclusion here is that LLMs are worse at formalizing than humans are. Additionally, for Lean 4 specifically, I don't think there's enough training data.

People are already using Prolog for this;

1) A series of excellent and detailed blog posts by Eugene Asahara Prolog in the LLM Era - https://eugeneasahara.com/category/prolog-in-the-llm-era/

2) Previous HN discussion Use Prolog to improve LLM's reasoning - https://news.ycombinator.com/item?id=41831735

3) User "bytebach" gives a nice example of using Prolog as an intermediate DSL in the prompt to an LLM so as to transform English declarative -> Imperative code - https://news.ycombinator.com/item?id=41549823

That's the approach we're taking to verify LLM-generated SQL code at http://sql.ai.

Essentially there is growing interest in the "formal" math community (combinatorics, mining, etc ..) to do exactly this.

I think a big issue with this approach is that the initial and last steps are prone to sycophancy: the machine wants you to believe it's getting the job done, which may lead it to do something correct-looking over something correct. The middle steps (correct-by-construction transformations) do not need an LLM at all. It's what a certified compiler does.

I think the way forward, for the immediate future, is to feed AI agents with a mixture of (hand-written) natural language and formal blueprints, then use as many mechanized analysis methods as possible on the generated code (from unit/regression testing to static analysis, and possibly more powerful software verification procedures). Potentially feed the output of these analyses back to the agents.

You should check out Math Academy. It'll give you as much math background as any engineering student and they aim to provide the equivalent of a full undergrad math degree in the next few years.