Automated reasoning sits at an exciting boundary between mathematics and computer science. It asks how far formal logic, carefully designed languages, and computation can go in representing and checking mathematical arguments.
My current interest is in learning how proof assistants such as Lean connect abstract foundations with practical verification. The subject feels especially compelling because it draws on logic, algorithms, complexity, and the craft of expressing ideas precisely enough for both humans and machines.
This blog will gradually collect notes from that exploration, along with related thoughts on graph theory, machine learning, programming projects, and technical communities at NISER.