We are pleased to announce that one of our researchers, MSc Eng. Łukasz Janiec from the Department of Cybernetics and Robotics, has been awarded in the Dell Technologies competition “AI on Your Desk. It’s Simple!”.

The competition attracted significant interest. A panel of experts consisting of Prof. Włodzisław Duch (Nicolaus Copernicus University), Dr. Maciej Kawecki (well-known science communicator promoting Polish researchers in Poland and abroad, This is The World and This is IT), and Sebastian Kondracki (one of the creators of Bielik AI) selected 15 projects from over 600 submissions to be awarded the modern local AI workstation Dell Pro Max with GB10.

The finalists were given the opportunity to meet at Dell Technologies headquarters in Łódź with experts and the director of Dell Poland, Dariusz Piotrkowski. The program also included site visits and on-site workshops at the factory. Each participant had the opportunity to present and consult their projects and plans for using the workstation.

Mr. Łukasz Janiec’s project assumes the use of the capabilities of this workstation within the initiative “Trustworthy Robotics by Design: Automation of Formal Verification of Robotics Algorithms using LLMs and Lean 4”, which is related to his research and doctoral dissertation work.

“I plan to use local LLM models to support the automatic formal verification of robotics algorithms and the underlying mathematics using Lean 4, a programming language and proof assistant in which mathematical proofs can be formalized and verified. The work will be based on tools such as LeanDojo, LeanProgress, and a novel approach called ‘Formal-Verification-in-the-Loop’ at the higher layer of the control system,” says MSc Eng. Łukasz Janiec about his plans. “Such work is particularly important in safety-critical robotic systems: surgical robots, real-time cyber-physical systems such as defensive drones, and multi-robot factory systems, where even short deadlocks can cause millions in production losses.”

Inspired by the excellent lecture “Mathematical discovery in the age of AI” by Dr. Bartosz Naskręcki, the researcher hopes to contribute to building robust and verified mathematical and algorithmic foundations for robotics that will support trustworthy artificial intelligence systems.

MSc Eng. Łukasz Janiec works on coordination and automatic synthesis of formally correct control in multi-robot systems. An important part of his research is the analysis and avoidance of deadlocks in RAS-type event-driven systems, conformal prediction for ensuring robustness under uncertainty, and formal verification of control correctness (Lean 4 + LLM).