Hard problems · Robotics · Research
Proving that a robot cannot reach its target
A research project that produces independently checkable mathematical proofs that a robot motion is impossible.
The problem
To plan a robot's motion, you search for a collision-free path. When you find one, all is well. When you don't, you can't tell whether no such path exists or whether you simply haven't searched long enough. This was already the problem that resisted during my PhD, in 2005. In industry, that uncertainty is costly: you don't know whether to keep searching, move the robot or redesign the cell layout.
The approach
Reframe the question: instead of searching for a path, search for a proof that no path exists.
Build the method and the demonstrator, on the model of a real 7-joint industrial arm (KUKA iiwa7).
Make every proof independently checkable: a small, separate program, using exact arithmetic, checks each proof without trusting the method that produced it.
Go further on guarantees: a second checker, written in Lean, whose own correctness is formally proven.
The result
Impossibility proofs checked by two independent verifiers, and an open-access paper with the code.
What's transferable
Knowing for certain that something is impossible can be worth as much as finding a solution: validating a workshop layout before investing, guaranteeing that a robot cannot reach a dangerous zone, avoiding weeks of fruitless search. More broadly, this is how I work with AI: it produces, and we build the means to check that what it produces is right.