Jukka Suomela's Avatar

Jukka Suomela

@jukkasuomela.fi

Associate Professor – Department of Computer Science, Aalto University – theory of distributed & parallel computing – https://jukkasuomela.fi

1,702
Followers
2,315
Following
2,856
Posts
18.10.2023
Joined
Posts Following

Latest posts by Jukka Suomela @jukkasuomela.fi

Don Knuth plays the organ. Photo credit Rajan P. Parrikar

Don Knuth plays the organ. Photo credit Rajan P. Parrikar

Get to know Don Knuth in this BEATCS Spring issue interview by Chen Avin and Stefan Schmid bulletin.eatcs.org/index.php/be...

10.03.2026 14:33 👍 2 🔁 2 💬 0 📌 2
Bulletin of EATCS

The Spring issue of the EATCS Bulletin is now available!

10.03.2026 14:30 👍 5 🔁 2 💬 0 📌 1

The EATCS Bulletin and YouTube crew are always looking for contributions 👩‍🔬 Especially junior folks are warmly invited to write or film something 🎥✍️

10.03.2026 15:06 👍 2 🔁 2 💬 0 📌 0
Preview
GitHub - suomela/fin-dep: Finitely dependent distributions Finitely dependent distributions. Contribute to suomela/fin-dep development by creating an account on GitHub.

This vibe-formalized project is now also fully kernel-checked. You can run "lake env leanchecker --fresh" to see there is no environment hacking, and there is a file that lets you easily also see that the main theorems only use the three standard axioms: github.com/suomela/fin-...

09.03.2026 18:08 👍 1 🔁 1 💬 0 📌 0

But there isn't really that much "behind the scenes" beyond what is said in the manuscript and the code repo. Most of the time was spent by me telling Codex "keep going", "continue", "go", "good, continue"… and occasionally feeding extra money. :)

07.03.2026 09:41 👍 1 🔁 0 💬 1 📌 0

There are these slides that contain something: jukkasuomela.fi/doc/theory-s...

07.03.2026 09:41 👍 1 🔁 0 💬 1 📌 0
GitHub - suomela/2-coloring-1-round: 2-Coloring Cycles in One Round: Formalization in Lean 4 2-Coloring Cycles in One Round: Formalization in Lean 4 - suomela/2-coloring-1-round

Lean 4 code here: github.com/suomela/2-co...

07.03.2026 07:42 👍 0 🔁 1 💬 0 📌 0
Preview
2-Coloring Cycles in One Round We show that there is a one-round randomized distributed algorithm that can 2-color cycles such that the expected fraction of monochromatic edges is less than 0.24118. We also show that a one-round al...

Here is now a short writeup on our chatbot-assisted proof that we also vibe-formalized: arxiv.org/abs/2603.04235

07.03.2026 07:42 👍 4 🔁 2 💬 2 📌 0
Post image

L'Aquila…

05.03.2026 18:48 👍 1 🔁 0 💬 0 📌 0
Post image

I never understood why Dropbox is so painfully slow to synchronize photos. Apparently this setting fixes everything. Why isn't this the default setting?

05.03.2026 17:46 👍 2 🔁 0 💬 0 📌 0
Post image

L'Aquila…

01.03.2026 19:54 👍 4 🔁 1 💬 0 📌 0
Post image Post image Post image Post image

L'Aquila…

01.03.2026 19:54 👍 9 🔁 2 💬 1 📌 0
Preview
Is a LOCAL algorithm computable? Common definitions of the "standard" LOCAL model tend to be sloppy and even self-contradictory on one point: do the nodes update their state using an arbitrary function or a computable function? So fa...

Another new paper on arXiv: arxiv.org/abs/2602.21022

25.02.2026 10:42 👍 2 🔁 3 💬 0 📌 0

Puolet täynnä muutamassa viikossa.

Vielä tarvitaan kuitenkin nimiä alle.

Autonominen ATK! Suvereeni serverihuone! Itsenäinen IT!

www.kansalaisaloite.fi/fi/aloite/16...

24.02.2026 08:04 👍 56 🔁 16 💬 1 📌 0
Preview
It does not matter how you define locally checkable labelings Locally checkable labeling problems (LCLs) form the foundation of the modern theory of distributed graph algorithms. First introduced in the seminal paper by Naor and Stockmeyer [STOC 1993], these are...

Another new paper on arXiv: arxiv.org/abs/2602.18188

23.02.2026 19:21 👍 1 🔁 1 💬 0 📌 0
Preview
Classification of Local Optimization Problems in Directed Cycles We present a complete classification of the distributed computational complexity of local optimization problems in directed cycles for both the deterministic and the randomized LOCAL model. We show th...

A new paper on arXiv:
arxiv.org/abs/2602.13046

23.02.2026 19:20 👍 1 🔁 1 💬 0 📌 0
Preview
GitHub - suomela/fin-dep: Finitely dependent distributions Finitely dependent distributions. Contribute to suomela/fin-dep development by creating an account on GitHub.

Here is a small research project that I did recently with chatbots: github.com/suomela/fin-... — everything is vibe-formalized in Lean 4 (approx. 24500 lines of Lean code).

20.02.2026 08:42 👍 2 🔁 2 💬 0 📌 0
Call for Papers 40th International Symposium on Distributed Computing November 9-13, 2026 Rome, Italy https://www.disc-conference.org/wp/disc2026/ ## **DISC Conference Overview** The International Symposium on Distributed Computing (DISC) is an international forum on the theory, design, analysis, implementation and application of distributed systems and networks. It is organized in cooperation with the European Association for Theoretical Computer Science (EATCS). The symposium was established **41 years ago** , in 1985, as a biannual International Workshop on Distributed Algorithms on Graphs (WDAG). ## **Important Dates** **Paper registration:** May 27, 2026 **Submission deadline:** June 1, 2026 **Rebuttal phase:** July 21-25, 2026 **Notification:** August 5, 2026 All deadlines are at 23:59 AoE. ## **Scope** Submissions are sought in all areas of distributed algorithms and distributed systems, including theory, design, implementation, modelling, analysis, and application of distributed systems and networks. Topics of interest include, but are not limited to: – Biological and nature-inspired distributed algorithms – Blockchain protocols – Distributed and concurrent data structures, replication and consistency – Distributed graph algorithms – Distributed machine learning and data science – Distributed operating systems, middleware, database systems – Experimental evaluation of distributed algorithms and systems – Fault tolerance, reliability, availability – Formal methods for distributed computing: verification, synthesis and testing – Game-theoretic and knowledge-based approaches to distributed computing – High-performance, cloud and grid computing – Internet and Web applications, social networks and recommendation systems – Mobile agents, autonomous distributed systems, swarm robotics – Multiprocessor and multi-core architectures and algorithms – Population protocols and chemical reaction networks – Quantum distributed algorithms – Security in distributed computing, cryptographic protocols – Self-stabilizing, self-organizing, and autonomous systems – Synchronization, persistence and transactional memory – Wireless, mobile, sensor and ad-hoc networks ## **Submissions** A submitted paper should clearly motivate the importance of the problem being addressed, discuss prior work and its relationship to the paper, explicitly and precisely state the paper’s key contributions, and outline the key technical ideas and methods used to achieve the main claims. A submission should strive to be accessible to a broad audience, as well as having sufficient details for experts in the area. There are two types of submissions: regular papers and brief announcements. Regular papers must report on original research that has not previously been published (and may not be concurrently submitted to other journals or conferences with proceedings). All ideas necessary for an expert to fully verify the central claims in a paper, including experimental results, should be included in the submission. A brief announcement may describe work in progress or work presented elsewhere. A brief announcement may also present a result that is short and elegant but does not require a longer paper. It may also be used to announce a software distribution or an experimental result of interest that can be concisely described. The title of a brief announcement must start with the phrase “Brief Announcement: “. A paper that is not accepted as a regular paper may be invited as a brief announcement. When requested by the program committee, each author of the submitted paper(s) is expected to prepare a professional review of a non-conflicted DISC 2026 submission that falls within their research expertise. Submission should be done via the following web page: https://disc26.hotcrp.com ## **Submission format** Submissions must be in English in pdf format and they must be prepared using the LaTeX style template for LIPIcs (https://submission.dagstuhl.de/series/details/5#author) with `\documentclass[a4paper,anonymous,USenglish]{lipics-v2021}.` Submissions must be anonymous, without any author names, affiliations, or email addresses. The contact information of the authors will be entered separately in the submission metadata. For regular papers, there is no page limit, and authors are encouraged to use the “full version” of their paper as the submission. The initial 15 pages, excluding the title page and a table of contents, should contain a clear presentation of the merits of the paper, including a discussion of the paper’s importance within the context of prior work and a description of the key technical and conceptual ideas used to achieve its main claims. (Illustrative figures are encouraged.) The submission must contain all necessary details, including full proofs of all claims in the paper. Although there is no bound on the length of a submission, material other than the first 15 pages, excluding the title page and a table of contents, will be read at the committee’s discretion. Papers submitted as brief announcements should comply with the above rules, replacing 15 pages with 5 pages. Submissions not conforming to the submission guidelines and papers outside of the scope of the conference will be rejected without consideration. All accept/reject decisions made by the program committee are final. ## **Use of Large Language Models (LLMs)** The use of LLMs for submission preparation is permitted, although it is highly recommended that they only be used for cosmetic changes, e.g. proofreading of the text. The use of LLMs in technical parts should be treated in the same way as any other software or system, and thus carefully described and documented in the submission. Ultimately, the authors are responsible for the content of their submission, and mis-use of LLM may result in rejection. Any questions about the LLM use policy should be directed to the PC chair, Keren Censor-Hillel (ckeren@cs.technion.ac.il). ## **Anonymous Submissions** We will use a relaxed implementation of double-blind peer review. Submissions must not reveal the identity of the authors in any way. In particular, authors’ names and affiliation should not appear in the document itself. Authors should ensure that any references to their own related work are in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”). The purpose of this process is to help PC members and external reviewers come to an initial judgment about the paper without bias, not to make it impossible for them to discover the authors if they were to try. You are free to disseminate your work through arXiv and other online repositories and give presentations on your work as usual. Moreover, nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult. In particular, important references should not be omitted or anonymized. Brief announcements should also be submitted without author names and affiliations so that a reviewer can form an initial judgment without bias, but they can contain a reference to the full version of the work in the bibliography. Please feel free to ask the PC chair if you have any questions about the double-blind policy of DISC 2026. ## **Conflict of Interest** The submission form provides an opportunity to specify conflicts of interest with any of the PC members and other member of research community. A conflict of interest is limited to the following: – A family member or close friend; – A Ph.D. advisor or advisee (no time limit), or postdoctoral or undergraduate mentor or mentee within the past five years; – A person with the same affiliation; – A person involved in an alleged incident of harassment; – Frequent collaborators, or collaborators who have jointly published papers within the last two years. If you feel that you have a valid reason for a conflict of interest beyond listed above, or any other issues related to the fair treatment of your submission, contact the PC chair, Keren Censor-Hillel (ckeren@cs.technion.ac.il), or the SafeTOC representative for DISC, listed a https://safetoc.org/index.php/toc-advisors/. ## **Participation at DISC** It is expected that accepted papers and brief announcements be presented in-person at the conference. ## **Publication** The proceedings will be published by LIPIcs. The final version of the paper has to be formatted following the LIPIcs guidelines. Regular papers will have 15 pages in the final proceedings (excluding references), and brief announcements will have 5 pages in the proceedings (including everything). If more space is needed, the authors are encouraged to post the full version e.g. on arXiv and refer to it in their paper. Accepted papers and brief announcements must be presented by one of the authors, with a full registration and according to the final schedule. Extended and revised versions of selected papers will be considered for a special issue of the journal Distributed Computing. The best paper at DISC will be considered for publication in the Journal of the ACM. ## **Awards** Awards will be given to the best paper and the best student paper. To be eligible for the best student paper award, at least one of the paper authors must be a full-time student at the time of submission, and the student(s) must have made a significant contribution to the paper.

DISC 2026 call for papers:
https://www.disc-conference.org/wp/disc2026/call-for-papers/

17.02.2026 13:25 👍 1 🔁 2 💬 0 📌 0

Here are the slides of the invited talk I gave on Friday at SOFSEM 2026: jukkasuomela.fi/doc/sofsem-2...

14.02.2026 11:26 👍 1 🔁 0 💬 0 📌 0

… but such "autoformalization pipelines" already exist today! All that you need to do is to type "formalize this in Lean 4" in Codex/GPT-5.3, and surprisingly often it delivers.

14.02.2026 07:14 👍 1 🔁 0 💬 0 📌 0

… where it says: "Future research must focus on building autoformalization pipelines that automatically translate LLM-generated informal mathematics into formal verification languages (such as Lean, Coq, or Isabelle)" …

14.02.2026 07:14 👍 0 🔁 0 💬 1 📌 0

What caught my attention is that this paper mentions formalization as a "future direction" in Section 9.2…

14.02.2026 07:14 👍 0 🔁 0 💬 1 📌 0
Preview
Accelerating Scientific Research with Gemini: Case Studies and... Recent advances in large language models (LLMs) have opened new avenues for accelerating scientific research. While models are increasingly capable of assisting with routine tasks, their ability...

Google put out an article on accelerating research with Gemini. I'm one of the 34 authors for my adventures in vibe-coding a research paper.

04.02.2026 20:47 👍 9 🔁 1 💬 1 📌 0
STOC 2026 - 58th ACM Symposium on Theory of Computing

The list of accepted papers at #STOC2026 is out:
acm-stoc.org/stoc2026/acc...

Congratulations to all authors!

13.02.2026 01:27 👍 27 🔁 9 💬 0 📌 0
Preview
Teknologia | Suomalaisprofessorin ajatuskoe paljastaa tekoälyn rajat Lupaukset Albert Einsteinin tasoisesta tekoälystä eivät ole toteutuneet. Nykyiset tekoälyn heikkoudet paljastuvat yksinkertaisessa ajatuskokeessa, jonka suomalaisprofessori Teppo Felin esittää.

Hesari väittää, että "nykyisellä tekoälyllä ei pysty luomaan oikeasti uutta tiedettä". Jään miettimään, mitähän se sitten on, mitä me tekoälyllä teemme, jos ei "oikeasti uutta tiedettä"?
www.hs.fi/visio/art-20...

12.02.2026 21:48 👍 4 🔁 0 💬 4 📌 0
Post image

64 × 1024 = 65536. I could get used to this calculator. It was surprisingly quick and easy to use even for a beginner.

12.02.2026 10:44 👍 7 🔁 0 💬 0 📌 1

Maanantaina PODC 2026 -submission deadline, siihen mennessä pitäisi olla valmiina, sen jälkeen voisi laittaa arXiviin…

10.02.2026 17:59 👍 1 🔁 0 💬 0 📌 0
Preview
Testaa itsesi | Älä valehtele itsellesi, kuinka keski-ikäinen oikeasti olet Todellisen ikänsä tarkistaminen ei ole koskaan ollut niin helppoa kuin nyt.

“Oikaisu 10.2. kello 19.09: Juppi on 1980-luvun urasuuntautunut kaupunkilainen, ei nimitys vasikan suoliliepeelle, kuten testissä aiemmin kerrottiin.” www.hs.fi/kulttuuri/ar...

10.02.2026 17:52 👍 3 🔁 1 💬 1 📌 0
Preview
Liian helppo elämä. Teknologia poisti kitkan, ja nyt kärsimme siitä. ”Teknologia muuttaa jotain meidän sisällä olevaa, eikä se tunnu hyvältä”, sanoo filosofi.

Lukusuositus (ei tarjoa ratkaisuita mutta herättää ajatuksia):
www.uusijuttu.fi/juttu/sUyCW4...

09.02.2026 18:52 👍 5 🔁 0 💬 0 📌 0
Post image

Palkkaamme suomea osaavia lehtoreita: www.aalto.fi/fi/avoimet-t...

09.02.2026 09:25 👍 3 🔁 1 💬 0 📌 0