Formally Writing Mathematics for Automatic Reasoning
How do you interpret a piece of written math such as x = x/2 + 2? Is it an equation to be solved for the unknown x? A logical statement to be assessed for truth? Or an assignment that updates the value of x?
If you’re unsure, the confusion isn’t your fault. The problem lies in the informal conventions of mathematical writing, where readers are expected to “read between the lines.” In this lecture, we’ll explore formal mathematical writing — a method that removes ambiguity, making mathematical intent clear not just for humans, but also for computational tools and AI engines.
You’ll learn how to use quantifiers and logical structures to precisely express mathematical meaning. We’ll also discuss how such formalism plays a foundational role in writing provable software.
Finally, you’ll get a hands-on glimpse of Lean, a leading interactive theorem prover that demonstrates how formal mathematics powers modern automated reasoning.
By the end of this lecture, you’ll be writing math with greater precision — and discovering deep connections between mathematics, computing, and software.
About the Speaker:
Dr. Mukhtar Ullah earned his BS in Electrical Engineering with Distinction from UET Peshawar in 1999. He began his career as Assistant Manager (Electronics) at NESCOM, Islamabad (2000–2001), before receiving the prestigious TROSS award, which enabled him to complete an MS in Advanced Control and Systems Engineering with Distinction from the University of Manchester.
In 2003, he joined the University of Rostock, Germany, as a Research Scientific Officer, where he completed his PhD in Systems Biology in 2009. He continued at Rostock as a postdoctoral researcher until 2013. That year, he returned to Pakistan and joined FAST–National University of Computer and Emerging Sciences, where he currently serves as Professor and Dean of Engineering.
His PhD research focused on stochastic modeling of uncertainty in systems biology and bioinformatics. Dr. Ullah has authored a Springer textbook and published over 40 papers in international journals and conferences across diverse fields, including computational biology, control systems, signal processing, power systems, automation, telemetry, remote sensing, agriculture, and engineering education.
He has supervised six PhD students and eight MS students, and is currently advising four PhD candidates. In addition, he has mentored more than 15 undergraduate final-year projects in Electrical Engineering. He maintains active research collaborations with NESCOM, the University of Rostock (Germany), the University of Hull (UK), and the University of Lincoln (USA), working on topics ranging from artificial intelligence and control systems to statistical modeling.
Dr. Mukhtar Ullah is also deeply engaged in academic quality assurance and policy development. He regularly evaluates academic programs and research proposals for the Pakistan Engineering Council, Higher Education Commission, and Pakistan Science Foundation. He contributes to curriculum development and assessment processes at leading institutions including NUST, GIKI, PIEAS and UET Taxila.
This session is free and open to all. Just visit the venue to attend it.
The Black Hole
Plot 5H, Street 100, G-11/3, Islamabad.
Click here for Google Maps Location
