EAST labs and hackathon in Bangalore
Siddhartha Gadgil
Dear All,
An announcement that may be of interest to you.
regards,
Siddhartha
Delighted to announce the launch of Emergence Autonomous Systems Lab in Bangalore. We will work on using Lean to greatly enhance reliability of autonomous agentic AI systems.
Specifically, we will work on enabling the application of Lean to a range of systems related to the real world, science and mathematics. This will involve both developing core Lean tooling and building many domain specific libraries and tools.
A second focus will be to extend Lean to systems where full autoformalization is not possible, including systems that are not closed and/or do not have known ground truths. Even for these Lean can allow separating loginc from external knowledge and assumptions and encapsulating these. Further reasoning can be better organised and abstracted.
Thirdly, being based in Bangalore with its strong software community and being closely associated with the Indian Institute of Science, we will work towards building up Lean, especially for programming and for industry, in India.
Working part time with us will be (our "Cambridge unit") @Anand Rao Tadipatri and @Siddharth Bhat . If you would like to join us, please feel free to contact us through the website or to DM me here on Zulip.
We will have a hackathon on LeanLang for Verified Autonomy in Bangalore. This will have a two-day in person phase on April 17 and 18 at the Indian Institute of Science, Bangalore followed by 10 days of online work.
The hackathon is the kick-off event of the new Emergence Autonomous Systems lab. Details of the hackathon are as follows:
Proved Guardrails in Lean for Multi-Agent Systems
Multi-agent systems such as those built on OpenClaw have become extremely popular because of their power across many domains. However, they also introduce significant risks. These risks must be addressed without sacrificing the capabilities that make such systems valuable. Guardrails backed by formal proofs are a natural way to ensure safety without being excessively restrictive. This hackathon is focused on building such verification systems in the Lean Prover.
The hackathon will begin with a one-day workshop on Lean, focused mainly on programming and the basic metaprogramming needed to build these systems. This will be followed by one day of in-person guided project work, and then 10 days of online interaction to complete the projects.
Participants will develop a model of a class of multi-agent systems like OpenClaw in Lean, together with the basic theory needed to reason about them. They will define types, terms, and functions that capture the semantics of these systems in Lean, and prove the core theorems on which proof automation can build. To interface with the Lean code, they may also extend Lean's syntax and build connections to proof automation tools. Participants may choose the style of agentic system they want to formalize, including specialized systems such as those for mathematics.
A successful project will be able to verify correct behaviour and flag risks within a powerful agentic system, without being so defensive that it weakens the system's usefulness. All code will be open-sourced (with acknowledgement of the hackathon sponsor) and should be well documented. After the hackathon, we aim to aggregate the various contributions into a common system.