diff --git a/client/package.json b/client/package.json
index 3bd4bc8b..b5e6952e 100644
--- a/client/package.json
+++ b/client/package.json
@@ -26,7 +26,10 @@
     "react-split": "^2.0.14",
     "react": "^19.2.0",
     "tailwindcss": "^4.1.18",
-    "vscode-ws-jsonrpc": "^3.5.0"
+    "vscode-ws-jsonrpc": "^3.5.0",
+    "y-monaco": "^0.1.6",
+    "y-webrtc": "^10.3.0",
+    "yjs": "^13.6.30"
   },
   "devDependencies": {
     "@codingame/esbuild-import-meta-url-plugin": "^1.0.3",
diff --git a/client/src/App.tsx b/client/src/App.tsx
index 153fb034..987a24bd 100644
--- a/client/src/App.tsx
+++ b/client/src/App.tsx
@@ -1,4 +1,5 @@
 import './css/App.css'
+import './css/Collab.css'
 import './css/Editor.css'
 
 import { faCode } from '@fortawesome/free-solid-svg-icons'
@@ -8,14 +9,26 @@ import { useAtom } from 'jotai/react'
 import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
 import * as monaco from 'monaco-editor'
 import * as path from 'path'
-import { useCallback, useEffect, useRef, useState } from 'react'
+import { useCallback, useEffect, useMemo, useRef, useState } from 'react'
 import Split from 'react-split'
+import { MonacoBinding } from 'y-monaco'
+import { WebrtcProvider } from 'y-webrtc'
+import * as Y from 'yjs'
 
 import LeanLogo from './assets/logo.svg'
 import { codeAtom } from './editor/code-atoms'
+import { NavButton } from './navigation/NavButton'
 import { Menu } from './navigation/Navigation'
+import RotatingGlobe from './navigation/RotatingGlobe'
+import LeaveCollaborationPopup from './Popups/LeaveCollaboration'
 import { mobileAtom, settingsAtom } from './settings/settings-atoms'
 import { lightThemes } from './settings/settings-types'
+import {
+  collabDisplayNameAtom,
+  collabPasswordAtom,
+  collabRoomAtom,
+  isCollaboratingAtom,
+} from './store/collaboration-atoms'
 import { importedCodeAtom } from './store/import-atoms'
 import { currentProjectAtom } from './store/project-atoms'
 import { screenWidthAtom } from './store/window-atoms'
@@ -37,8 +50,18 @@ function App() {
   const [, setScreenWidth] = useAtom(screenWidthAtom)
   const [project] = useAtom(currentProjectAtom)
   const [code, setCode] = useAtom(codeAtom)
+  const ydoc = useMemo(() => new Y.Doc(), [])
+  const [provider, setProvider] = useState<WebrtcProvider | null>(null)
+  const [binding, setBinding] = useState<MonacoBinding | null>(null)
+  const [collabRoom] = useAtom(collabRoomAtom)
+  const [collabDisplayName] = useAtom(collabDisplayNameAtom)
+  const [collabPassword] = useAtom(collabPasswordAtom)
+  const [usersInCollab, setUsersInCollab] = useState(0)
+  const [isCollaborating] = useAtom(isCollaboratingAtom)
   const [importedCode] = useAtom(importedCodeAtom)
 
+  const [leaveCollabOpen, setLeaveCollabOpen] = useState(false)
+
   const model = editor?.getModel()
 
   // Lean4monaco options
@@ -66,6 +89,59 @@ function App() {
     return () => window.removeEventListener('resize', handleResize)
   }, [setScreenWidth])
 
+  // clean up ydoc on unmount
+  useEffect(() => {
+    return () => ydoc.destroy()
+  }, [ydoc])
+
+  // this effect manages the lifetime of the Yjs document and the provider
+  useEffect(() => {
+    // const provider = new WebsocketProvider('wss://demos.yjs.dev/ws', roomname, ydoc)
+    // See https://github.com/yjs/y-webrtc for options
+    if (!isCollaborating || !collabRoom) {
+      setProvider(null)
+      return
+    }
+
+    const signalingUrl =
+      (window.location.protocol === 'https:' ? 'wss://' : 'ws://') +
+      window.location.host +
+      '/yjs-signaling'
+    console.log('[Lean4web] collab signaling url:', signalingUrl)
+
+    const provider = new WebrtcProvider(collabRoom, ydoc, {
+      maxConns: 50,
+      password: collabPassword,
+      signaling: [signalingUrl],
+      filterBcConns: true,
+    })
+    if (collabDisplayName) {
+      provider.awareness.setLocalStateField('user', { name: collabDisplayName })
+    }
+    setProvider(provider)
+    return () => {
+      provider?.destroy()
+    }
+  }, [ydoc, isCollaborating, collabRoom, collabDisplayName, collabPassword])
+
+  // this effect manages the lifetime of the editor binding
+  useEffect(() => {
+    if (provider == null || editor == null) {
+      return
+    }
+    console.log('reached', provider)
+    const binding = new MonacoBinding(
+      ydoc.getText(),
+      editor.getModel()!,
+      new Set([editor]),
+      provider?.awareness,
+    )
+    setBinding(binding)
+    return () => {
+      binding.destroy()
+    }
+  }, [ydoc, provider, editor])
+
   // Update LeanMonaco options when preferences are loaded or change
   useEffect(() => {
     if (!project) return
@@ -259,10 +335,33 @@ function App() {
     }
   }, [handleKeyDown, handleKeyUp])
 
+  // keep the number of people in the room updated
+  useEffect(() => {
+    if (!provider) return
+    const update = () => {
+      setUsersInCollab(provider.awareness.getStates().size)
+    }
+    provider.awareness.on('change', update)
+    update()
+    return () => {
+      provider.awareness.off('change', update)
+    }
+  }, [provider])
+
   return (
     <div className="app monaco-editor">
       <nav>
         <LeanLogo />
+        {isCollaborating && (
+          <NavButton
+            iconElement={<RotatingGlobe />}
+            text={`${collabDisplayName} ∈ ${collabRoom} (${usersInCollab})`}
+            className="leave-collab-button"
+            onClick={() => {
+              setLeaveCollabOpen(true)
+            }}
+          />
+        )}
         <Menu
           setContent={setContent}
           restart={leanMonaco?.restart}
@@ -322,6 +421,12 @@ function App() {
           </p>
         </div>
       </Split>
+      <LeaveCollaborationPopup
+        open={leaveCollabOpen}
+        handleClose={() => {
+          setLeaveCollabOpen(false)
+        }}
+      />
     </div>
   )
 }
diff --git a/client/src/Popups/Collaboration.tsx b/client/src/Popups/Collaboration.tsx
new file mode 100644
index 00000000..264f2627
--- /dev/null
+++ b/client/src/Popups/Collaboration.tsx
@@ -0,0 +1,103 @@
+import { useAtom } from 'jotai'
+import { FormEvent, useState } from 'react'
+
+import { Popup } from '../navigation/Popup'
+import {
+  collabDisplayNameAtom,
+  collabPasswordAtom,
+  collabRoomAtom,
+  isCollaboratingAtom,
+} from '../store/collaboration-atoms'
+
+/** The popup to join a collaboration room. */
+function CollaborationPopup({ open, handleClose }: { open: boolean; handleClose: () => void }) {
+  const [collabRoom, setCollabRoom] = useAtom(collabRoomAtom)
+  const [collabDisplayName, setCollabDisplayName] = useAtom(collabDisplayNameAtom)
+  const [collabPassword, setCollabPassword] = useAtom(collabPasswordAtom)
+  const [, setIsCollaborating] = useAtom(isCollaboratingAtom)
+  const [collabError, setCollabError] = useState('')
+
+  function onSubmit(ev: FormEvent) {
+    ev.preventDefault()
+    const isValid = /^[\w\d]{3,20}$/
+    const isValidPwd = /^[\w\d]{1,20}$/
+    if (!isValid.test(collabRoom)) {
+      setCollabError('Room name must be 3-20 alphanumeric characters.')
+      return
+    }
+    if (collabPassword != undefined && !isValidPwd.test(collabPassword)) {
+      setCollabError('The password must be up to 20 alphanumeric characters.')
+      return
+    }
+    if (!isValid.test(collabDisplayName)) {
+      setCollabError('Display name must be 3-20 alphanumeric characters.')
+      return
+    }
+    setCollabError('')
+    if (collabRoom) {
+      setIsCollaborating(true)
+      handleClose()
+    }
+  }
+
+  return (
+    <Popup open={open} handleClose={handleClose}>
+      <h2>Start or join collaboration</h2>
+      <form onSubmit={onSubmit}>
+        <div>
+          <p>
+            Others can join the collaboration by using the same "room name". The "display name" can
+            be chosen freely.
+          </p>
+          <p>
+            An optional password can be provided to restrict room access. Note that supplying a
+            different password will not result in an error. Instead each combination of room name
+            and password will have its own room.
+          </p>
+        </div>
+        <label>Room name:</label>
+        <input
+          required
+          autoFocus
+          type="text"
+          placeholder="Room name"
+          value={collabRoom}
+          onChange={(e) => {
+            setCollabRoom(e.target.value)
+            setCollabError('')
+          }}
+        />
+        <label>Display name:</label>
+        <input
+          required
+          type="text"
+          placeholder="Your display name"
+          value={collabDisplayName}
+          onChange={(e) => {
+            setCollabDisplayName(e.target.value)
+            setCollabError('')
+          }}
+        />
+        <label>Password (optional):</label>
+        <input
+          type="password"
+          placeholder="room password"
+          value={collabPassword}
+          onChange={(e) => {
+            const pwd = e.target.value
+            if (pwd.length == 0) {
+              setCollabPassword(undefined)
+            } else {
+              setCollabPassword(pwd)
+            }
+            setCollabError('')
+          }}
+        />
+        {collabError && <p className="form-error">{collabError}</p>}
+        <input type="submit" value="Join" />
+      </form>
+    </Popup>
+  )
+}
+
+export default CollaborationPopup
diff --git a/client/src/Popups/LeaveCollaboration.tsx b/client/src/Popups/LeaveCollaboration.tsx
new file mode 100644
index 00000000..55e6ca96
--- /dev/null
+++ b/client/src/Popups/LeaveCollaboration.tsx
@@ -0,0 +1,44 @@
+import { useAtom } from 'jotai'
+import { FormEvent } from 'react'
+
+import { Popup } from '../navigation/Popup'
+import { collabRoomAtom, isCollaboratingAtom } from '../store/collaboration-atoms'
+
+/** The popup to join a collaboration room. */
+function LeaveCollaborationPopup({
+  open,
+  handleClose,
+}: {
+  open: boolean
+  handleClose: () => void
+}) {
+  const [, setIsCollaborating] = useAtom(isCollaboratingAtom)
+  const [collabRoom] = useAtom(collabRoomAtom)
+
+  function onSubmit(ev: FormEvent) {
+    ev.preventDefault()
+    setIsCollaborating(false)
+    handleClose()
+  }
+
+  return (
+    <Popup open={open} handleClose={handleClose}>
+      <h2>{`Leave collaboration '${collabRoom}'?`}</h2>
+      <form onSubmit={onSubmit}>
+        <div className="button-row">
+          <button
+            onClick={(ev) => {
+              ev.preventDefault()
+              handleClose()
+            }}
+          >
+            Stay
+          </button>
+          <input type="submit" value="Leave" />
+        </div>
+      </form>
+    </Popup>
+  )
+}
+
+export default LeaveCollaborationPopup
diff --git a/client/src/Popups/LoadZulip.tsx b/client/src/Popups/LoadZulip.tsx
index 40ea15fd..69999db9 100644
--- a/client/src/Popups/LoadZulip.tsx
+++ b/client/src/Popups/LoadZulip.tsx
@@ -50,7 +50,7 @@ function LoadZulipPopup({
         Copy paste a zulip message here to extract code-blocks.{' '}
         <i>(mobile: "copy to clipboard", web: "view message source")</i>
       </p>
-      {error ? <p className="form-error">{error}</p> : null}
+      {error && <p className="form-error">{error}</p>}
       <form onSubmit={handleLoad}>
         <textarea
           name="Zulip message input"
diff --git a/client/src/Popups/PrivacyPolicy.tsx b/client/src/Popups/PrivacyPolicy.tsx
index 5d38f566..25f80d24 100644
--- a/client/src/Popups/PrivacyPolicy.tsx
+++ b/client/src/Popups/PrivacyPolicy.tsx
@@ -8,13 +8,16 @@ function PrivacyPopup({ open, handleClose }: { open: boolean; handleClose: () =>
       <h2>Privacy Policy</h2>
 
       <p>
-        Our server collects metadata (such as IP address, browser, operating system) and the data
-        that the user enters into the editor. The data is used to compute the Lean output and
+        Our server collects metadata (such as IP address, browser, operating system) and the content
+        which the user enters into the editor. The data is used to compute the Lean output and
         display it to the user. The information will be stored as long as the user stays on our
         website and will be deleted immediately afterwards. We keep logs to improve our software,
-        but the contained data is anonymised.
+        but the contained data is anonymised and does not contain user code.
+      </p>
+      <p>
+        The collaboration feature keeps an in-memory list of active rooms. The content is then
+        shared directly peer-to-peer and therefore not stored on the server.
       </p>
-
       <p>
         We don't use cookies but you can choose to save the settings in the browser store by
         activating the option in the settings.
diff --git a/client/src/css/Collab.css b/client/src/css/Collab.css
new file mode 100644
index 00000000..0c5235b9
--- /dev/null
+++ b/client/src/css/Collab.css
@@ -0,0 +1,22 @@
+.yRemoteSelection {
+  background-color: color-mix(in srgb, var(--vscode-symbolIcon-eventForeground) 25%, transparent);
+  border: 1px solid var(--vscode-contrastActiveBorder); /* for high-contrast theme */
+}
+
+.yRemoteSelectionHead {
+  position: absolute;
+  border-left: var(--vscode-symbolIcon-eventForeground) solid 2px;
+  border-top: var(--vscode-symbolIcon-eventForeground) solid 2px;
+  border-bottom: var(--vscode-symbolIcon-eventForeground) solid 2px;
+  height: 100%;
+  box-sizing: border-box;
+}
+
+.yRemoteSelectionHead::after {
+  position: absolute;
+  content: ' ';
+  border: 3px solid var(--vscode-symbolIcon-eventForeground);
+  border-radius: 4px;
+  left: -4px;
+  top: -5px;
+}
diff --git a/client/src/css/Modal.css b/client/src/css/Modal.css
index 54fec037..ab4be5c4 100644
--- a/client/src/css/Modal.css
+++ b/client/src/css/Modal.css
@@ -53,9 +53,17 @@ input[type='file'] {
   }
 }
 
+.modal form {
+  display: flex;
+  flex-direction: column;
+  gap: 0.5rem;
+}
+
 .modal input[type='text'],
+.modal input[type='password'],
 .modal textarea {
   width: 100%;
+  box-sizing: border-box;
 }
 
 .modal textarea {
@@ -64,7 +72,7 @@ input[type='file'] {
 
 .modal .form-error {
   color: var(--vscode-editorError-foreground);
-  font-weight: bold;
+  font-size: 14px;
 }
 
 .modal input[type='submit'],
@@ -85,6 +93,7 @@ input[type='file'] {
 }
 
 .modal input[type='text'],
+.modal input[type='password'],
 .modal select {
   padding: 10px 12px;
 
@@ -94,12 +103,12 @@ input[type='file'] {
   color: var(--vscode-input-foreground);
 }
 
-.modal input[type='text'] {
+.modal input[type='password'] {
   font-family: 'JuliaMono';
 }
 
 .modal #abbreviationCharacter {
-  width: 15px;
+  width: 35px;
   margin-left: 4px;
 }
 
@@ -138,3 +147,7 @@ a {
   text-decoration: none;
   color: var(--vscode-textLink-foreground);
 }
+
+.button-row {
+  display: flex;
+}
diff --git a/client/src/css/Navigation.css b/client/src/css/Navigation.css
index dc155427..e2214599 100644
--- a/client/src/css/Navigation.css
+++ b/client/src/css/Navigation.css
@@ -89,6 +89,29 @@ nav select:hover {
   background-color: var(--vscode-menu-selectionBackground);
 }
 
+nav .nav-link.leave-collab-button {
+  animation: pulse 5s cubic-bezier(0.4, 0, 0.6, 1) infinite;
+}
+
+nav .nav-link.leave-collab-button span {
+  font-size: 0.8rem;
+}
+
+nav .nav-link.leave-collab-button:hover {
+  color: unset;
+  background-color: unset;
+}
+
+@keyframes pulse {
+  0%,
+  100% {
+    opacity: 1;
+  }
+  50% {
+    opacity: 0.5;
+  }
+}
+
 .tooltip {
   position: relative;
   cursor: pointer;
diff --git a/client/src/navigation/NavButton.tsx b/client/src/navigation/NavButton.tsx
index a7a1920e..49c0286e 100644
--- a/client/src/navigation/NavButton.tsx
+++ b/client/src/navigation/NavButton.tsx
@@ -1,28 +1,27 @@
 import { IconDefinition } from '@fortawesome/free-solid-svg-icons'
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
-import { JSX, MouseEventHandler } from 'react'
+import { JSX } from 'react'
 
 /** A button to appear in the hamburger menu or to navigation bar. */
 export function NavButton({
   icon,
   iconElement,
   text,
-  title,
-  onClick = () => {},
-  href = undefined,
+  ...props
 }: {
   icon?: IconDefinition
   iconElement?: JSX.Element
   text: string
-  title?: string
-  onClick?: MouseEventHandler<HTMLAnchorElement>
-  href?: string
-}) {
+} & React.AnchorHTMLAttributes<HTMLAnchorElement>) {
   // note: it seems that we can just leave the `target="_blank"` and it has no
   // effect on links without a `href`. If not, add `if (href)` statement here...
   return (
-    <a className="nav-link" title={title} onClick={onClick} href={href!} target="_blank">
-      {iconElement ?? <FontAwesomeIcon icon={icon!} />}&nbsp;{text}
+    <a
+      {...props}
+      className={props.className ? `nav-link ${props.className}` : 'nav-link'}
+      target="_blank"
+    >
+      {iconElement ?? <FontAwesomeIcon icon={icon!} />}&nbsp;<span>{text}</span>
     </a>
   )
 }
diff --git a/client/src/navigation/Navigation.tsx b/client/src/navigation/Navigation.tsx
index d38b7c94..54c4c4d8 100644
--- a/client/src/navigation/Navigation.tsx
+++ b/client/src/navigation/Navigation.tsx
@@ -21,6 +21,7 @@ import { ChangeEvent, Dispatch, SetStateAction, useState } from 'react'
 import { lean4webConfig } from '../../config'
 import ZulipIcon from '../assets/zulip.svg'
 import { codeAtom } from '../editor/code-atoms'
+import CollaborationPopup from '../Popups/Collaboration'
 import ImpressumPopup from '../Popups/Impressum'
 import LoadUrlPopup from '../Popups/LoadUrl'
 import LoadZulipPopup from '../Popups/LoadZulip'
@@ -28,11 +29,13 @@ import PrivacyPopup from '../Popups/PrivacyPolicy'
 import ToolsPopup from '../Popups/Tools'
 import { mobileAtom } from '../settings/settings-atoms'
 import { SettingsPopup } from '../settings/SettingsPopup'
+import { isCollaboratingAtom } from '../store/collaboration-atoms'
 import { setImportUrlAndProjectAtom } from '../store/import-atoms'
 import { currentProjectAtom, projectsAtom, visibleProjectsAtom } from '../store/project-atoms'
 import { save } from '../utils/SaveToFile'
 import { Dropdown } from './Dropdown'
 import { NavButton } from './NavButton'
+import RotatingGlobe from './RotatingGlobe'
 
 /** The menu items either appearing inside the dropdown or outside */
 function FlexibleMenu({
@@ -45,6 +48,7 @@ function FlexibleMenu({
   setContent,
   setLoadUrlOpen,
   setLoadZulipOpen,
+  setJoinCollabOpen,
 }: {
   isInDropdown: boolean
   setOpenNav: Dispatch<SetStateAction<boolean>>
@@ -55,7 +59,10 @@ function FlexibleMenu({
   setContent: (code: string) => void
   setLoadUrlOpen: Dispatch<SetStateAction<boolean>>
   setLoadZulipOpen: Dispatch<SetStateAction<boolean>>
+  setJoinCollabOpen: Dispatch<SetStateAction<boolean>>
 }) {
+  const ENABLE_COLLAB = import.meta.env.VITE_COLLAB != 'false'
+  const [isCollaborating] = useAtom(isCollaboratingAtom)
   const [, setImportUrlAndProject] = useAtom(setImportUrlAndProjectAtom)
   const [{ data: projects }] = useAtom(projectsAtom)
   const loadFileFromDisk = (event: ChangeEvent<HTMLInputElement>) => {
@@ -139,6 +146,15 @@ function FlexibleMenu({
           }}
         />
       </Dropdown>
+      {ENABLE_COLLAB && !isCollaborating && (
+        <NavButton
+          iconElement={<RotatingGlobe />}
+          text="Collaborate"
+          onClick={() => {
+            setJoinCollabOpen(true)
+          }}
+        />
+      )}
     </>
   )
 }
@@ -165,6 +181,7 @@ export function Menu({
   const [openLoad, setOpenLoad] = useState(false)
   const [loadUrlOpen, setLoadUrlOpen] = useState(false)
   const [loadZulipOpen, setLoadZulipOpen] = useState(false)
+  const [joinCollabOpen, setJoinCollabOpen] = useState(false)
 
   // state for the popups
   const [privacyOpen, setPrivacyOpen] = useState(false)
@@ -215,6 +232,7 @@ export function Menu({
           setContent={setContent}
           setLoadUrlOpen={setLoadUrlOpen}
           setLoadZulipOpen={setLoadZulipOpen}
+          setJoinCollabOpen={setJoinCollabOpen}
         />
       )}
       <Dropdown
@@ -237,6 +255,7 @@ export function Menu({
             setContent={setContent}
             setLoadUrlOpen={setLoadUrlOpen}
             setLoadZulipOpen={setLoadZulipOpen}
+            setJoinCollabOpen={setJoinCollabOpen}
           />
         )}
         <NavButton
@@ -305,6 +324,12 @@ export function Menu({
         handleClose={() => setLoadZulipOpen(false)}
         setContent={setContent}
       />
+      <CollaborationPopup
+        open={joinCollabOpen}
+        handleClose={() => {
+          setJoinCollabOpen(false)
+        }}
+      />
     </div>
   )
 }
diff --git a/client/src/navigation/RotatingGlobe.tsx b/client/src/navigation/RotatingGlobe.tsx
new file mode 100644
index 00000000..7643d199
--- /dev/null
+++ b/client/src/navigation/RotatingGlobe.tsx
@@ -0,0 +1,27 @@
+import {
+  faGlobeAfrica,
+  faGlobeAmericas,
+  faGlobeAsia,
+  faGlobeEurope,
+  faGlobeOceania,
+} from '@fortawesome/free-solid-svg-icons'
+import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
+
+function getGlobeIcon(timezone: string) {
+  if (!timezone) return faGlobeEurope
+
+  if (timezone.startsWith('Africa')) return faGlobeAfrica
+  if (timezone.startsWith('America')) return faGlobeAmericas
+  if (timezone.startsWith('Europe')) return faGlobeEurope
+  if (timezone.startsWith('Asia')) return faGlobeAsia
+  if (timezone.startsWith('Australia') || timezone.startsWith('Pacific')) return faGlobeOceania
+  return faGlobeEurope
+}
+
+/** Globe Icon, rotated to fit the user's timezone */
+export default function RotatingGlobe() {
+  const timezone = Intl.DateTimeFormat().resolvedOptions().timeZone
+  const icon = getGlobeIcon(timezone)
+
+  return <FontAwesomeIcon icon={icon} />
+}
diff --git a/client/src/store/collaboration-atoms.ts b/client/src/store/collaboration-atoms.ts
new file mode 100644
index 00000000..22768390
--- /dev/null
+++ b/client/src/store/collaboration-atoms.ts
@@ -0,0 +1,9 @@
+import { atom } from 'jotai'
+
+export const collabRoomAtom = atom('')
+
+export const collabDisplayNameAtom = atom('')
+
+export const collabPasswordAtom = atom<string>()
+
+export const isCollaboratingAtom = atom(false)
diff --git a/client/vite.config.ts b/client/vite.config.ts
index 10ae5465..42d02bba 100644
--- a/client/vite.config.ts
+++ b/client/vite.config.ts
@@ -62,6 +62,10 @@ export default defineConfig({
         target: "ws://localhost:8080",
         ws: true,
       },
+      "/yjs-signaling": {
+        target: "ws://localhost:8080",
+        ws: true,
+      },
       "/api": {
         target: "http://localhost:8080",
       },
diff --git a/doc/Installation.md b/doc/Installation.md
index 05ea6d7b..2e4c7e91 100644
--- a/doc/Installation.md
+++ b/doc/Installation.md
@@ -106,9 +106,9 @@ The following environment variables can be used to modify the server
 
 For example for `npm start`, `npm start:client`.
 
-| name   | values | default | description |
-| ------ | ------ | ------- | ----------- |
-| (none) |        |         |             |
+| name          | values          | default | description                      |
+| ------------- | --------------- | ------- | -------------------------------- |
+| `VITE_COLLAB` | `true`, `false` | `true`  | Enable the collaboration feature |
 
 #### Server
 
@@ -117,6 +117,7 @@ For example for `npm start`, `npm run production`, `npm run start:server`.
 | name                 | values                      | default         | description                                                                                                                                       |
 | -------------------- | --------------------------- | --------------- | ------------------------------------------------------------------------------------------------------------------------------------------------- |
 | `NO_BWRAP`           | `true`, `false`             | `false`         | to disable to use of `bubblewrap` in production mode. This means `Lean` runs without any container on your system, which imposes a security risk! |
+| `VITE_COLLAB`        | `true`, `false`             | `true`          | Enable the collaboration feature                                                                                                                  |
 | `GITHUB_ACTIONS`     | `true` ,`false`             | `false`         | is set by github actions to change the verbosity of some server output                                                                            |
 | `NODE_ENV`           | `development`, `production` |                 |                                                                                                                                                   |
 | `PROJECTS_BASE_PATH` | string                      | `Projects`      | **relative path** from the root of this repo to the folder where the Lean projects are located.                                                   |
diff --git a/doc/Usage.md b/doc/Usage.md
index 5c97b005..af24ba89 100644
--- a/doc/Usage.md
+++ b/doc/Usage.md
@@ -45,3 +45,9 @@ The recognised settings are:
 - Non-boolean settings:
 - `abbreviationCharacter`: lead character for unicode abbreviations. values: a character. default: `\`
 - `theme`: selection between one light and dark theme. More themes are available in the settings, but they cannot be set through the URL. values: `light` or `dark`. default: `light` (TODO: infererred from browser)
+
+### Collaboration
+
+The collaboration feature allows to simultaneously view and edit code across multiple users. The code is still synchronised with the URL-arguments as described above, the collaboration connection simply ensures all connected browsers are updated synchonously.
+
+A shared connection is established when users start a collaboration room with the same room name and password. If one user creates "TestRoom" without a password and the other user "TestRoom" with password "123", they will be in two distinct collaboration rooms.
diff --git a/ecosystem.config.cjs b/ecosystem.config.cjs
index 3b36c711..d6e05f91 100644
--- a/ecosystem.config.cjs
+++ b/ecosystem.config.cjs
@@ -8,6 +8,7 @@ module.exports = {
         NODE_ENV: "production",
         PORT: 8001,
         NO_BWRAP: false,
+        VITE_COLLAB: true,
         PROJECTS_BASE_PATH: "Projects", // relative path to the folder containing all projects
         SSL_CRT_FILE: undefined,
         SSL_KEY_FILE: undefined,
diff --git a/package-lock.json b/package-lock.json
index 3f93b93e..814fd031 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -59,7 +59,10 @@
         "react-dom": "^19.2.0",
         "react-split": "^2.0.14",
         "tailwindcss": "^4.1.18",
-        "vscode-ws-jsonrpc": "^3.5.0"
+        "vscode-ws-jsonrpc": "^3.5.0",
+        "y-monaco": "^0.1.6",
+        "y-webrtc": "^10.3.0",
+        "yjs": "^13.6.30"
       },
       "devDependencies": {
         "@codingame/esbuild-import-meta-url-plugin": "^1.0.3",
@@ -4390,7 +4393,6 @@
       "version": "1.5.1",
       "resolved": "https://registry.npmjs.org/base64-js/-/base64-js-1.5.1.tgz",
       "integrity": "sha512-AKpaYlHn8t4SVbOHCy+b5+KKgvR4vrsD8vbvrbiQJps7fKDTkjkDry6ji0rUJjC0kzbNePLwzxq8iypo41qeWA==",
-      "dev": true,
       "funding": [
         {
           "type": "github",
@@ -5795,6 +5797,12 @@
         "url": "https://github.com/fb55/entities?sponsor=1"
       }
     },
+    "node_modules/err-code": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/err-code/-/err-code-3.0.1.tgz",
+      "integrity": "sha512-GiaH0KJUewYok+eeY05IIgjtAe4Yltygk9Wqp1V5yVWLdhf0hYZchRjNIT9bb0mSwRcIusT3cx7PJUf3zEIfUA==",
+      "license": "MIT"
+    },
     "node_modules/error-ex": {
       "version": "1.3.2",
       "resolved": "https://registry.npmjs.org/error-ex/-/error-ex-1.3.2.tgz",
@@ -6983,6 +6991,12 @@
         "node": ">=6.9.0"
       }
     },
+    "node_modules/get-browser-rtc": {
+      "version": "1.1.0",
+      "resolved": "https://registry.npmjs.org/get-browser-rtc/-/get-browser-rtc-1.1.0.tgz",
+      "integrity": "sha512-MghbMJ61EJrRsDe7w1Bvqt3ZsBuqhce5nrn/XAwgwOXhcsz53/ltdxOse1h/8eKXj5slzxdsz56g5rzOFSGwfQ==",
+      "license": "MIT"
+    },
     "node_modules/get-caller-file": {
       "version": "2.0.5",
       "resolved": "https://registry.npmjs.org/get-caller-file/-/get-caller-file-2.0.5.tgz",
@@ -7436,7 +7450,6 @@
       "version": "1.2.1",
       "resolved": "https://registry.npmjs.org/ieee754/-/ieee754-1.2.1.tgz",
       "integrity": "sha512-dcyqhDvX1C46lXZcVqCpK+FtMRQVdIMN6/Df5js2zouUsqG7I6sFxitIC+7KYK29KdXOLHdu9zL4sFnoVQnqaA==",
-      "dev": true,
       "funding": [
         {
           "type": "github",
@@ -8105,6 +8118,16 @@
         "node": ">=10"
       }
     },
+    "node_modules/isomorphic.js": {
+      "version": "0.2.5",
+      "resolved": "https://registry.npmjs.org/isomorphic.js/-/isomorphic.js-0.2.5.tgz",
+      "integrity": "sha512-PIeMbHqMt4DnUP3MA/Flc0HElYjMXArsw1qwJZcm9sqR8mq3l8NYizFMty0pWwE/tzIGH3EKK5+jes5mAr85yw==",
+      "license": "MIT",
+      "funding": {
+        "type": "GitHub Sponsors ❤",
+        "url": "https://github.com/sponsors/dmonad"
+      }
+    },
     "node_modules/isstream": {
       "version": "0.1.2",
       "resolved": "https://registry.npmjs.org/isstream/-/isstream-0.1.2.tgz",
@@ -8439,6 +8462,27 @@
         "node": ">= 0.8.0"
       }
     },
+    "node_modules/lib0": {
+      "version": "0.2.117",
+      "resolved": "https://registry.npmjs.org/lib0/-/lib0-0.2.117.tgz",
+      "integrity": "sha512-DeXj9X5xDCjgKLU/7RR+/HQEVzuuEUiwldwOGsHK/sfAfELGWEyTcf0x+uOvCvK3O2zPmZePXWL85vtia6GyZw==",
+      "license": "MIT",
+      "dependencies": {
+        "isomorphic.js": "^0.2.4"
+      },
+      "bin": {
+        "0ecdsa-generate-keypair": "bin/0ecdsa-generate-keypair.js",
+        "0gentesthtml": "bin/gentesthtml.js",
+        "0serve": "bin/0serve.js"
+      },
+      "engines": {
+        "node": ">=16"
+      },
+      "funding": {
+        "type": "GitHub Sponsors ❤",
+        "url": "https://github.com/sponsors/dmonad"
+      }
+    },
     "node_modules/lightningcss": {
       "version": "1.30.2",
       "resolved": "https://registry.npmjs.org/lightningcss/-/lightningcss-1.30.2.tgz",
@@ -10031,11 +10075,30 @@
         "node": ">=0.4.x"
       }
     },
+    "node_modules/queue-microtask": {
+      "version": "1.2.3",
+      "resolved": "https://registry.npmjs.org/queue-microtask/-/queue-microtask-1.2.3.tgz",
+      "integrity": "sha512-NuaNSa6flKT5JaSYQzJok04JzTL1CA6aGhv5rfLW3PgqA+M2ChpZQnAC8h8i4ZFkBS8X5RqkDBHA7r4hej3K9A==",
+      "funding": [
+        {
+          "type": "github",
+          "url": "https://github.com/sponsors/feross"
+        },
+        {
+          "type": "patreon",
+          "url": "https://www.patreon.com/feross"
+        },
+        {
+          "type": "consulting",
+          "url": "https://feross.org/support"
+        }
+      ],
+      "license": "MIT"
+    },
     "node_modules/randombytes": {
       "version": "2.1.0",
       "resolved": "https://registry.npmjs.org/randombytes/-/randombytes-2.1.0.tgz",
       "integrity": "sha512-vYl3iOX+4CKUWuxGi9Ukhie6fsqXqS9FE2Zaic4tNFD2N2QQaXOMFbuKK4QmDHC0JO6B1Zp41J0LpT0oR68amQ==",
-      "dev": true,
       "license": "MIT",
       "dependencies": {
         "safe-buffer": "^5.1.0"
@@ -10141,7 +10204,6 @@
       "version": "3.6.2",
       "resolved": "https://registry.npmjs.org/readable-stream/-/readable-stream-3.6.2.tgz",
       "integrity": "sha512-9u/sniCrY3D5WdsERHzHE4G2YCXqoG5FTHUiCC4SIbr6XcLZBY05ya9EKjYek9O5xOAwjGq+1JdGBAS7Q9ScoA==",
-      "dev": true,
       "license": "MIT",
       "dependencies": {
         "inherits": "^2.0.3",
@@ -10450,7 +10512,6 @@
       "version": "5.2.1",
       "resolved": "https://registry.npmjs.org/safe-buffer/-/safe-buffer-5.2.1.tgz",
       "integrity": "sha512-rp3So07KcdmmKbGvgaNxQSJr7bGVSVk5S9Eq1F+ppbRo70+YeaDxkw5Dd8NPN+GD6bjnYm2VuPuCXmpuYvmCXQ==",
-      "dev": true,
       "funding": [
         {
           "type": "github",
@@ -10793,6 +10854,59 @@
       "dev": true,
       "license": "ISC"
     },
+    "node_modules/simple-peer": {
+      "version": "9.11.1",
+      "resolved": "https://registry.npmjs.org/simple-peer/-/simple-peer-9.11.1.tgz",
+      "integrity": "sha512-D1SaWpOW8afq1CZGWB8xTfrT3FekjQmPValrqncJMX7QFl8YwhrPTZvMCANLtgBwwdS+7zURyqxDDEmY558tTw==",
+      "funding": [
+        {
+          "type": "github",
+          "url": "https://github.com/sponsors/feross"
+        },
+        {
+          "type": "patreon",
+          "url": "https://www.patreon.com/feross"
+        },
+        {
+          "type": "consulting",
+          "url": "https://feross.org/support"
+        }
+      ],
+      "license": "MIT",
+      "dependencies": {
+        "buffer": "^6.0.3",
+        "debug": "^4.3.2",
+        "err-code": "^3.0.1",
+        "get-browser-rtc": "^1.1.0",
+        "queue-microtask": "^1.2.3",
+        "randombytes": "^2.1.0",
+        "readable-stream": "^3.6.0"
+      }
+    },
+    "node_modules/simple-peer/node_modules/buffer": {
+      "version": "6.0.3",
+      "resolved": "https://registry.npmjs.org/buffer/-/buffer-6.0.3.tgz",
+      "integrity": "sha512-FTiCpNxtwiZZHEZbcbTIcZjERVICn9yq/pDFkTl95/AxzD1naBctN7YO68riM/gLSDY7sdrMby8hofADYuuqOA==",
+      "funding": [
+        {
+          "type": "github",
+          "url": "https://github.com/sponsors/feross"
+        },
+        {
+          "type": "patreon",
+          "url": "https://www.patreon.com/feross"
+        },
+        {
+          "type": "consulting",
+          "url": "https://feross.org/support"
+        }
+      ],
+      "license": "MIT",
+      "dependencies": {
+        "base64-js": "^1.3.1",
+        "ieee754": "^1.2.1"
+      }
+    },
     "node_modules/simple-update-notifier": {
       "version": "2.0.0",
       "resolved": "https://registry.npmjs.org/simple-update-notifier/-/simple-update-notifier-2.0.0.tgz",
@@ -10933,7 +11047,6 @@
       "version": "1.3.0",
       "resolved": "https://registry.npmjs.org/string_decoder/-/string_decoder-1.3.0.tgz",
       "integrity": "sha512-hkRX8U1WjJFd8LsDJ2yQ/wWWxaopEsABU1XfkM8A+j0+85JAGppt16cr1Whg6KIbb4okU6Mql6BOj+uup/wKeA==",
-      "dev": true,
       "license": "MIT",
       "dependencies": {
         "safe-buffer": "~5.2.0"
@@ -11820,7 +11933,6 @@
       "version": "1.0.2",
       "resolved": "https://registry.npmjs.org/util-deprecate/-/util-deprecate-1.0.2.tgz",
       "integrity": "sha512-EPD5q1uXyFxJpCrLnCc1nHnq3gOa6DZBocAIiI2TaSCA7VCJ1UJDMagCzIkXNsUYfD1daK//LTEQ8xiIbrHtcw==",
-      "dev": true,
       "license": "MIT"
     },
     "node_modules/uuid": {
@@ -12346,6 +12458,70 @@
         "node": ">=0.4"
       }
     },
+    "node_modules/y-monaco": {
+      "version": "0.1.6",
+      "resolved": "https://registry.npmjs.org/y-monaco/-/y-monaco-0.1.6.tgz",
+      "integrity": "sha512-sYRywMmcylt+Nupl+11AvizD2am06ST8lkVbUXuaEmrtV6Tf+TD4rsEm6u9YGGowYue+Vfg1IJ97SUP2J+PVXg==",
+      "license": "MIT",
+      "dependencies": {
+        "lib0": "^0.2.43"
+      },
+      "engines": {
+        "node": ">=12.0.0",
+        "npm": ">=6.0.0"
+      },
+      "peerDependencies": {
+        "monaco-editor": ">=0.20.0",
+        "yjs": "^13.3.1"
+      }
+    },
+    "node_modules/y-protocols": {
+      "version": "1.0.7",
+      "resolved": "https://registry.npmjs.org/y-protocols/-/y-protocols-1.0.7.tgz",
+      "integrity": "sha512-YSVsLoXxO67J6eE/nV4AtFtT3QEotZf5sK5BHxFBXso7VDUT3Tx07IfA6hsu5Q5OmBdMkQVmFZ9QOA7fikWvnw==",
+      "license": "MIT",
+      "dependencies": {
+        "lib0": "^0.2.85"
+      },
+      "engines": {
+        "node": ">=16.0.0",
+        "npm": ">=8.0.0"
+      },
+      "funding": {
+        "type": "GitHub Sponsors ❤",
+        "url": "https://github.com/sponsors/dmonad"
+      },
+      "peerDependencies": {
+        "yjs": "^13.0.0"
+      }
+    },
+    "node_modules/y-webrtc": {
+      "version": "10.3.0",
+      "resolved": "https://registry.npmjs.org/y-webrtc/-/y-webrtc-10.3.0.tgz",
+      "integrity": "sha512-KalJr7dCgUgyVFxoG3CQYbpS0O2qybegD0vI4bYnYHI0MOwoVbucED3RZ5f2o1a5HZb1qEssUKS0H/Upc6p1lA==",
+      "license": "MIT",
+      "dependencies": {
+        "lib0": "^0.2.42",
+        "simple-peer": "^9.11.0",
+        "y-protocols": "^1.0.6"
+      },
+      "bin": {
+        "y-webrtc-signaling": "bin/server.js"
+      },
+      "engines": {
+        "node": ">=12"
+      },
+      "funding": {
+        "type": "GitHub Sponsors ❤",
+        "url": "https://github.com/sponsors/dmonad"
+      },
+      "optionalDependencies": {
+        "ws": "^8.14.2"
+      },
+      "peerDependencies": {
+        "yjs": "^13.6.8"
+      }
+    },
     "node_modules/y18n": {
       "version": "5.0.8",
       "resolved": "https://registry.npmjs.org/y18n/-/y18n-5.0.8.tgz",
@@ -12403,6 +12579,23 @@
         "fd-slicer": "~1.1.0"
       }
     },
+    "node_modules/yjs": {
+      "version": "13.6.30",
+      "resolved": "https://registry.npmjs.org/yjs/-/yjs-13.6.30.tgz",
+      "integrity": "sha512-vv/9h42eCMC81ZHDFswuu/MKzkl/vyq1BhaNGfHyOonwlG4CJbQF4oiBBJPvfdeCt/PlVDWh7Nov9D34YY09uQ==",
+      "license": "MIT",
+      "dependencies": {
+        "lib0": "^0.2.99"
+      },
+      "engines": {
+        "node": ">=16.0.0",
+        "npm": ">=8.0.0"
+      },
+      "funding": {
+        "type": "GitHub Sponsors ❤",
+        "url": "https://github.com/sponsors/dmonad"
+      }
+    },
     "node_modules/yocto-queue": {
       "version": "0.1.0",
       "resolved": "https://registry.npmjs.org/yocto-queue/-/yocto-queue-0.1.0.tgz",
diff --git a/server/index.mjs b/server/index.mjs
index 62d193ac..3ac42018 100755
--- a/server/index.mjs
+++ b/server/index.mjs
@@ -27,7 +27,8 @@ const __dirname = url.fileURLToPath(new URL(".", import.meta.url));
 const environment = process.env.NODE_ENV;
 const isGithubAction = process.env.GITHUB_ACTIONS;
 const isDevelopment = environment === "development";
-const NO_BWRAP = process.env.NO_BWRAP?.toLowerCase() === "true" ?? false;
+const NO_BWRAP = process.env.NO_BWRAP?.toLowerCase() == "true" ?? false;
+const ENABLE_COLLAB = process.env.VITE_COLLAB?.toLowerCase() != "false" ?? true;
 
 const crtFile = process.env.SSL_CRT_FILE;
 const keyFile = process.env.SSL_KEY_FILE;
@@ -228,11 +229,130 @@ function FilenamesToUri(prefix, obj) {
   return obj;
 }
 
+if (ENABLE_COLLAB) {
+  console.log("[Lean4web]: enabling signaling server for collaboration.");
+}
+
+const yjsTopics = new Map(); // roomName -> Set<Connection>
+
+const sendYjs = (conn, message) => {
+  if (conn.readyState !== 0 && conn.readyState !== 1) {
+    conn.close();
+  }
+  try {
+    conn.send(JSON.stringify(message));
+  } catch (e) {
+    conn.close();
+  }
+};
+
+const setupYjsConnection = (conn, req) => {
+  const ip = req
+    ? req.headers["x-forwarded-for"] || req.socket.remoteAddress
+    : "unknown";
+  console.log(`[Lean4web]: new collab connection established from ${ip}`);
+  const subscribedTopics = new Set();
+  let closed = false;
+  // Check if connection is still alive
+  let pongReceived = true;
+  const pingInterval = setInterval(() => {
+    if (!pongReceived) {
+      conn.close();
+      clearInterval(pingInterval);
+    } else {
+      pongReceived = false;
+      try {
+        conn.ping();
+      } catch (e) {
+        conn.close();
+      }
+    }
+  }, 30000);
+  conn.on("pong", () => {
+    pongReceived = true;
+  });
+  conn.on("close", () => {
+    console.log(`[Lean4web]: collab connection closed from ${ip}`);
+    subscribedTopics.forEach((topicName) => {
+      const subs = yjsTopics.get(topicName) || new Set();
+      subs.delete(conn);
+      if (subs.size === 0) {
+        yjsTopics.delete(topicName);
+      }
+    });
+    subscribedTopics.clear();
+    closed = true;
+  });
+  conn.on("message", (message) => {
+    if (typeof message === "string" || message instanceof Buffer) {
+      try {
+        message = JSON.parse(message);
+      } catch (e) {
+        return;
+      }
+    }
+    if (message && message.type && !closed) {
+      switch (message.type) {
+        case "subscribe":
+          (message.topics || []).forEach((topicName) => {
+            if (typeof topicName === "string") {
+              let topic = yjsTopics.get(topicName);
+              if (!topic) {
+                topic = new Set();
+                yjsTopics.set(topicName, topic);
+              }
+              topic.add(conn);
+              subscribedTopics.add(topicName);
+              console.log(
+                `[Lean4web]: client subscribed to collab topic: ${topicName}`,
+              );
+            }
+          });
+          break;
+        case "unsubscribe":
+          (message.topics || []).forEach((topicName) => {
+            const subs = yjsTopics.get(topicName);
+            if (subs) {
+              subs.delete(conn);
+              console.log(
+                `[Lean4web]: client unsubscribed from collab topic: ${topicName}`,
+              );
+            }
+          });
+          break;
+        case "publish":
+          if (message.topic) {
+            const receivers = yjsTopics.get(message.topic);
+            console.log(
+              `[lean4web]: client published to collab topic ${message.topic} (receivers: ${receivers ? receivers.size : 0})`,
+            );
+            if (receivers) {
+              message.clients = receivers.size;
+              receivers.forEach((receiver) => sendYjs(receiver, message));
+            }
+          }
+          break;
+        case "ping":
+          sendYjs(conn, { type: "pong" });
+      }
+    }
+  });
+};
+
 wss.addListener("connection", async function (ws, req) {
   const urlRegEx = /^\/websocket\/([\w.-]+)$/;
   const reRes = urlRegEx.exec(req.url);
   if (!reRes) {
-    console.error(`Connection refused because of invalid URL: ${req.url}`);
+    if (
+      ENABLE_COLLAB &&
+      (req.url === "/yjs-signaling" || req.url === "/yjs-signaling/")
+    ) {
+      setupYjsConnection(ws, req);
+      return;
+    }
+    console.error(
+      `[Lean4web]: connection refused because of invalid URL: ${req.url}`,
+    );
     return;
   }
   const project = reRes[1];