Formalization

Everyday language is imprecise. The sentence “Large numbers are hard to divide” allows many interpretations. What does large mean, what does hard mean? Formalization means bringing such a statement into a form that permits only a single interpretation. Usually this is a formula, an equation, or a list of clear rules. In the process you lose some of the richness of language and gain unambiguity. This exact unambiguity is what a machine needs, since it cannot guess what was meant.

Why it matters

A computer does not check intentions, it checks symbols. As long as a problem is only described in words, it can’t do anything with it. Only the formal version makes it computable, provable, or verifiable.

This concerns far more than mathematics. A data retention law is formulated in words. Anyone who casts it into software has to decide on every unclear point. In doing so, contradictions surface that no one had noticed before. Formalization is therefore also a tool for thinking, not just for programming.

At the same time, this is a typical source of error. If the formal version misses the original concern, the system computes correctly on the wrong problem. The error then lies not in the code, but in the translation that preceded it.

How it works

The first step is defining the terms. You name the things involved and the properties that matter. For a class schedule, these would be classes, rooms, teachers, and time slots.

The second step is the conditions. What must hold, what is forbidden? A room must not be double-booked, every class needs exactly one math lesson per day. Such statements are written as precise rules, often using symbols for “and”, “or”, “for all”, and “there exists”.

The third step is the goal. What should be as good as possible? Few free periods, for example. Only once terms, conditions, and goal are fixed can a program systematically search for solutions.

A comparison helps: formalization is like a construction drawing made from a conversation with the client. The conversation contains wishes and hints. The drawing contains measurements in millimeters. Only with the drawing can someone build who wasn’t part of the conversation.

Where you encounter the term

In AI news, the word frequently comes up with models that are supposed to be capable of mathematics. Systems like AlphaProof work with formal proof languages, such as Lean. There, every step is machine-verifiable. The real hurdle is often translating a competition problem into this language in the first place. This is called autoformalization, when an AI takes on this translation itself.

Formalizations also appear in regulation. The EU’s AI legislation is followed by technical standards that turn vague terms like “high risk” into checkable criteria. Only then do companies know what they need to test.

In everyday life you encounter this principle in every form. An application forces you to squeeze your wishes into fields and checkboxes. This is uncomfortable and sometimes unfair, but it’s what makes processing possible in the first place. Formalization always carries this price: clarity in exchange for nuance.