Skip to content

Intelligent Input Bus (IBus)

For a comparison of IBus vs. XCompose, see the Linux section.

Background

There are multiple new input method frameworks for Wayland that replace the X keyboard extension (XKB). As of early 2026, the dominant framework is Intelligent Input Bus (IBus), which is the input method used by the GNOME desktop environment, but IBus can also be installed with other desktop environments.

This page focuses on using an IBus table input method. Many IBus input methods are built on top of ibus-table, including one for the abbreviations from the Lean VS Code extension. Alternative m17n input methods are listed at the end of this page.

Setup

Step 1: Install an input method for Lean

On Fedora

dnf install ibus-table-others

On other distros

If an ibus-table-others package is not available, you can install this input method from the lean.txt source file. The ibus-table package must be installed. It will already be installed on GNOME Desktop, but if not, install it (e.g., apt install ibus-table).

Using the lean.txt source file:

curl -O https://raw.githubusercontent.com/moebiuscurve/ibus-table-others/refs/heads/main/tables/lean.txt
sudo ibus-table-createdb --source lean.txt --name /usr/share/ibus-table/tables/lean.db
ibus restart

Step 2: Add Lean as an input source

On GNOME desktop

Go to Settings > Keyboard > Input Sources > + Add Input Source > ⋮ > type Lean > Other (Lean 4) > Add.

On non-GNOME desktops

Currently not documented here.

How to use

1) Switch to the Lean input method

On GNOME desktop, you can do this by simultaneously pressing super+space. The super key is the "Windows" key on most keyboards. Or you can use a mouse. Screenshots of GNOME's switchable input methods can be seen in Red Hat's documentation.

Important

Make sure the little box is checked to the left of the ∀ in the Lean input method icon. If not, tap the left-shift key. Tapping left-shift toggles whether table input mode is on or off.

2) Type

To input ∀α, type:

\ A L space \ A space

Tip

Even though the full abbreviation is all, you can just type al and it will auto-complete.

Note

A small pop-up window will appear to show possible completions and the symbols they will generate.

To input just a \, you can either tap left-shift to exit table input mode or type \ \ space.

Alternative m17n input methods

Multiple input method frameworks, such as IBus, support m17n input methods. Distinct m17n input methods will appear as separate input methods in your desktop environment, allowing you to quickly switch between them. When writing Lean, there are two types of math input methods to consider:

An input method of abbreviations from the Lean VS Code extension:
These key sequences are short and optimized for typing. If you write a lot of Lean, you'll want to learn and use these short key sequences.
An input method using LaTeX commands:
These key sequences are longer in the LaTeX-based input method, but easier to remember if you already know LaTeX.

Input method definition

Each m17n input method is defined by a .mim file. The m17n-db multilingualization database package/repository contains many ready-to-use m17n input methods. Users can customize their own m17n input method by creating a .mim file in their ~/.m17n.d/ directory, running ibus restart (or rebooting), and then adding it as a keyboard input source.

An input method using LaTeX commands

The math-latex.mim file from m17n-db defines an input method based on LaTeX commands. In GNOME, this input method appears as an "Input Source" named Other (t-math-latex (m17n)). You might need to install the ibus-m17n package for your Linux distro.

When using this keyboard, type a backslash (\) followed by a LaTeX (or LaTeX-like) command as a key sequence. See math-latex.mim for a full list of math symbols and key sequences.

An input method of Lean VS Code abbreviations

Warning

As of January 2026, the following m17n input methods for Lean are outdated and have probably not been packaged in any major distro.