We have cars driving on a 2-lane highway

There is a red lane and a blue lane

Each car has its own target lane where it wants to be at the next intersection

So some cars need to switch lanes

But what if we do not have space to switch lanes?

Some cars then need to slow down to make space

Assume we only switch lanes if we are currently in the wrong lane — what is the smallest possible number of maneuvers needed?

We want to minimize the “slow down” steps, and hence the average delay for traffic

Abstract version:
slide pebbles in a grid,
minimize the number of moves

Red

  • moves up and right
  • must end up in the top row

Blue

  • moves down and right
  • must end up in the bottom row
0 moves

Prior work (ATMOS 2018):
1.5-approximation

Red

  • moves up and right
  • must end up in the top row

Blue

  • moves down and right
  • must end up in the bottom row
0 moves

Prior work (ATMOS 2018):
1.5-approximation

0 moves

New: optimal solution in polynomial time

0 moves

New: optimal solution in polynomial time

red backlog
0
1
2
2
1
blue backlog
0
1
0
1
1
window
none
none
none
top
none
budget
0
0
0
1
0
total delay
0
1
4
6
6

We can compute the optimal number of delays with a transducer that keeps track of five values

New: optimal solution in polynomial time

red backlog
0
1
2
2
1
blue backlog
0
1
0
1
1
window
none
none
none
top
none
budget
0
0
0
1
0
total delay
0
1
4
6
6
Total moves (12)
= total delay (6)
+ pebbles that need
to change sides (6)

We can compute the optimal number of delays with a transducer that keeps track of five values

New: optimal solution in polynomial time

red backlog
0
1
2
2
1
blue backlog
0
1
0
1
1
window
none
none
none
top
none
budget
0
0
0
1
0
total delay
0
1
4
6
6

We can also reconstruct an optimal sequence from the table in polynomial time

Transducer

red = blue = total = budget = 0
window = None
allowed = { "top": {"2O", "22", "21"},
            "bottom": {"O1", "11", "21"} }
for c in columns:
    cost = { "OO": 0,          "1O": red,        "O1": red,
             "2O": blue,       "O2": blue,       "12": red + blue,
             "11": 2*red + 1,  "22": 2*blue + 1, "21": max(red + blue, 1) }[c]
    if window is None and c == "21":
        if blue == 0 and red >= 2:
            window, budget = "top", red - 1
        elif red == 0 and blue >= 2:
            window, budget = "bottom", blue - 1
    elif window is not None and c in allowed[window]:
        cost -= 1
        budget -= 1
        if budget == 0:
            window = None
    else:
        window, budget = None, 0
    red = max(red + c.count("1") - 1, 0)
    blue = max(blue + c.count("2") - 1, 0)
    if c == "21":
        red = max(red, 1)
        blue = max(blue, 1)
    total += cost

Research methods

  • Prior attempts:
    • GPT-5.2, 5.3, 5.4, 5.5, mostly in Codex
    • Claude Opus 4.8, mostly in Claude Code
  • Breakthrough:
    • Claude Fable 5 in Claude Code
  • Verification:
    • GPT-5.5 + Codex formalized the solution in Lean 4
  • Presentation:
    • GPT-5.5 + Codex with the help of reveal.js
  • With some human guidance by Jukka Suomela

Summary

  • Problem: changing lanes on a highway
  • Prior work: 1.5-approximation by human beings
  • New: optimal polynomial-time algorithm by chatbots