쌓인 기록에서 찾기
무엇을 찾으세요? 날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위 2026년 8월 13일 (목) 부터 2026년 9월 19일 (토)까지 674건
25건 · "증명"조건 지우기 ×
001 00:10 ▲ 255 · 댓글 176 Bend 2가 빠진 형식 검증의 표준 방식 Bend 2는 AI가 코드를 작성하고 증명을 통해 검증하는 언어로 소개되지만, 간단한 게임 규칙 검증에 442줄의 증명 코드를 필요로 한다. 오픈소스 · 도구 · Bend 2 and the Vibe-Coding Trap
Bend 2가 빠진 형식 검증의 표준 방식 Key Point 기존 형식 검증 분야의 성숙한 도구와 방식을 모르고 같은 문제를 더 복잡하게 재구성하는 것이 가능한 이유를 설명하며, 신생 언어/도구를 평가할 때 학문 기초의 중요성을 보여준다.
핵심 요약
Bend 2는 AI가 코드를 작성하고 증명을 통해 검증하는 언어로 소개되지만, 간단한 게임 규칙 검증에 442줄의 증명 코드를 필요로 한다. 저자는 이를 '비브 코딩의 함정'으로 지칭하며, 개발자가 충분한 분야 지식 없이 대규모 솔루션을 완성해 더 나은 방식을 놓친다고 비판한다. Bend의 웹페이지와 코드베이스에는 형식 검증(formal verification) 용어가 나타나지 않으며, 저자는 이 분야의 표준 언어인 SPARK로 동일한 프로그램을 작성해 12개 검사만으로 증명할 수 있음을 보인다. 저자의 핵심 주장은 Bend가 형식 검증이라는 기존 학문 분야의 표준 방식을 모르거나 간과한 채 복잡한 시스템을 새로 만들었다는 것이다. 002 09:10 ▲ 227 · 댓글 123 AI 실수 원천 차단하는 프로그래밍 언어 'Bend' 공개 형식 증명(proof)으로 AI가 작성한 코드의 정확성을 검증하는 프로그래밍 언어 Bend를 발표했다. AI · 머신러닝 · Bend – A language that blocks AI mistakes via proof, on CPU and GPU
AI 실수 원천 차단하는 프로그래밍 언어 'Bend' 공개 Key Point AI 에이전트가 코드를 자동 생성하는 시대에 형식 증명으로 보안 결함을 원천 차단할 수 있는 새로운 접근 방식을 제시하기 때문입니다.
핵심 요약
형식 증명(proof)으로 AI가 작성한 코드의 정확성을 검증하는 프로그래밍 언어 Bend를 발표했다. C 수준의 단일 코어 성능으로 컴파일되며, 동일 바이너리가 GPU에서 100배까지 빠르게 실행된다. 타입 체커가 증명 체커로 작동해 중간 규모 코드베이스에서 최대 1초 내에 검증을 완료한다. LAWS.bend 문법으로 지켜야 할 규칙을 선언하면, AI가 이를 위반하는 코드를 배포하지 못하도록 강제한다. 스레드나 락 없이 자동으로 병렬화되며, 메인 구현은 Linux와 macOS 기반이다. 003 06:10 ▲ 170 · 댓글 219 AI 시대, 수학의 본질을 놓치다 필즈상 수상자 25명이 서명한 AI 우려 공개서에 전 수상자 타오가 서명하지 않은 이유를 설명한 글이다. AI · 머신러닝 · Why I didn’t sign the Fields medallists’ letter
AI 시대, 수학의 본질을 놓치다 Key Point 현재 AI가 수학 연구에 미치는 영향을 둘러싼 관점의 차이를 보여주는데, 유명 수학자의 신중한 입장이 커뮤니티 내 다양한 견해를 반영합니다.
핵심 요약
필즈상 수상자 25명이 서명한 AI 우려 공개서에 전 수상자 타오가 서명하지 않은 이유를 설명한 글이다. 공개서는 AI가 문제 해결만 추구하면서 개념적 이해라는 수학의 본질 목표를 훼손할 수 있다고 주장한다. 타오는 이 관점에 완전히 동의하지 않으며, 수학자들 사이에 문제 해결과 개념적 이해의 중요도에 대한 다양한 스펙트럼이 존재한다고 본다. 자신의 자동정리증명 연구팀이 LLM의 진전으로 동기를 잃었지만, 인간이 정리를 증명하는 방식을 이해하는 것은 여전히 지적 가치가 있다고 말한다. 타오는 OpenAI로부터 금전적 지원을 받지 않았으며, 수학 커뮤니티가 AI를 둘러싸고 분열되는 것을 우려한다. 004 06:10 ▲ 104 · 댓글 30 CrowdSec, 5월 소스코드 유출 확인…고객 데이터는 무사 CrowdSec이 지난 5월 발생한 GitHub 저장소의 소스코드 유출을 9월 16일 확인했다. 보안 · CrowdSec Source Code Leak
CrowdSec, 5월 소스코드 유출 확인…고객 데이터는 무사 Key Point 보안 업체의 소스코드 유출은 심각해 보이지만, CrowdSec이 공개한 상황 설명에서 고객 데이터 피해와 보안 위험이 제한적인 이유를 구체적으로 확인할 수 있다.
핵심 요약
CrowdSec이 지난 5월 발생한 GitHub 저장소의 소스코드 유출을 9월 16일 확인했다. 유출된 것은 300개 저장소(130개+ 공개 저장소 포함) 중 비공개 부분으로, SaaS 콘솔 소스코드와 AWS 루틴, 커넥터, 자동화 코드다. 고객 데이터, 로그인 정보, 개인정보(PII) 등은 유출되지 않았으며 영향은 CrowdSec 내부에 제한된다. 유출 원인은 Mistral AI 사건과 유사하게 Tanstack 컴포넌트 침해로 추정되며, 이를 통해 API 키가 탈취돼 비공개 저장소 읽기 접근이 가능했다. 4개월간 코드가 크게 진화했고, CrowdSec은 네트워크 효과와 규모 에 의존하므로 코드 유출만으로는 실질적 피해가 제한적이며 모든 토큰과 자격증명을 즉시 교체했다. 005 21:11 당일 +140 로컬 머신에서 AI가 개발 도구를 직접 제어하는 WebCodex ChatGPT, Claude 등 AI 에이전트가 로컬 머신의 코드와 개발 도구에 직접 접근해 작업할 수 있게 해주는 Rust 기반 오픈소스 프로젝트다. AI · 머신러닝 · yyjeqhc/webcodex · Rust
로컬 머신에서 AI가 개발 도구를 직접 제어하는 WebCodex Key Point 개발자 머신을 떠나지 않으면서 AI 에이전트의 코딩 능력을 실제 개발 환경 전체에 활용할 수 있는 새로운 방식을 제시한다.
핵심 요약
ChatGPT, Claude 등 AI 에이전트가 로컬 머신의 코드와 개발 도구에 직접 접근해 작업할 수 있게 해주는 Rust 기반 오픈소스 프로젝트다. 코드 읽기·편집, 테스트·컴파일러 실행, Git 작업, 장시간 실행 작업 추적 등을 지원하며 코드를 클라우드에 옮길 필요가 없다. 데스크톱 앱(Windows·macOS) + OpenAI 보안 터널, CLI 기반 서버·러너, 임시 공유 등 다양한 배포 형태를 제공한다. 리포지토리 경계 내에서만 파일 읽기·수정·명령 실행이 가능하며, 버전 관리와 자격증명 보호를 강조한다. 006 18:10 ▲ 108 · 댓글 17 Rust 코드 수학적 정확성 검증하는 Verus 공개 Amazon이 개발한 오픈소스 자동 프로그램 검증 도구 Verus가 Rust 코드를 수학적 명세에 맞게 검증한다. 인프라 · 데브옵스 · Developing provably correct Rust code with Verus
Rust 코드 수학적 정확성 검증하는 Verus 공개 Key Point Rust의 타입 시스템만으로는 보장 불가한 로직 정확성을 형식적 증명으로 검증할 수 있는 새로운 도구로, 보안이 중요한 클라우드 인프라와 시스템 소프트웨어 개발에 영향을 미친다.
핵심 요약
Amazon이 개발한 오픈소스 자동 프로그램 검증 도구 Verus가 Rust 코드를 수학적 명세에 맞게 검증한다. 개발자가 Rust 소스 코드에 직접 전제 조건(requires)과 사후 조건(ensures) 주석을 추가하면, 모든 가능한 입력에 대해 코드가 명세와 일치하는지 기계적으로 확인한다. 테스트로 놓치기 쉬운 경계값 케이스도 포착하며, 피드백은 1초 이내에 나온다. Unsafe 코드와 동시성 코드의 정확성도 증명 가능하며, AWS Nitro Isolation Engine 등 성능 중시 코드에 적용된다. Amazon이 Kubernetes 컨트롤러, 인증서 검증 라이브러리 등 오픈소스 프로젝트에서도 사용 중이다. 007 03:10 ▲ 123 · 댓글 47 DeepSeek V4.1 Flash, AI 해킹 벤치마크에서 완벽한 성적 달성 DeepSeek V4.1 Flash가 Enclave의 AI 해킹 벤치마크에서 11개 취약한 타겟 모두에 코드 실행을 성공하고 4개의 보안 강화된 타겟은 모두 방어했다. AI · 머신러닝 · DeepSeek v4.1 Flash Is Now Our Best Hacking Model
DeepSeek V4.1 Flash, AI 해킹 벤치마크에서 완벽한 성적 달성 Key Point AI 모델이 보안 시스템을 얼마나 효과적으로 우회하는지 보여주며, 저가 토큰 캐싱으로 대규모 작업을 저렴하게 수행하는 기술의 실제 사례를 제시한다.
핵심 요약
DeepSeek V4.1 Flash가 Enclave의 AI 해킹 벤치마크에서 11개 취약한 타겟 모두에 코드 실행을 성공하고 4개의 보안 강화된 타겟은 모두 방어했다. 전체 공격에 $4.65만 소비했는데, 268.3백만 개의 입력 토큰 중 266.2백만 개가 캐시되어 저가격이 가능했다. 감사 결과 6개 공격은 설계된 경로를 따랐으나, 5개 공격은 테스트 환경의 예상 외 경로를 발견했다. Grafana는 90초 이내에 임시 플러그인 폴더에 실행 파일을 배치하는 대체 경로로 공략했고, Jenkins의 자격증명 읽기와 업로드 타이밍 공격도 성공했다. 벤치마크 시스템이 결과만 검증해선 부족하며, 공격 경로까지 확인해야 AI 에이전트의 실제 능력을 정확히 평가할 수 있다고 지적했다. 008 15:10 ▲ 102 · 댓글 35 수십 년 난제 'k-서버 추측' 마침내 증명 알고리즘 이론의 난제인 k-서버 추측이 증명됐다. 결정론적 온라인 알고리즘이 모든 메트릭 공간에서 경쟁비 k를 달성할 수 있다는 내용이다. AI · 머신러닝 · The k-server conjecture is true
수십 년 난제 'k-서버 추측' 마침내 증명 Key Point 온라인 알고리즘 이론에서 장기간 미해결이었던 핵심 추측의 증명으로, 경쟁적 분석 분야의 기초를 정립하는 중요한 진전이다.
핵심 요약
알고리즘 이론의 난제인 k-서버 추측이 증명됐다. 결정론적 온라인 알고리즘이 모든 메트릭 공간에서 경쟁비 k를 달성할 수 있다는 내용이다. 증명에는 일함수(work function) 알고리즘이 사용됐다. 이를 행렬의 대수적 표현으로 변환해 모든 가능한 경로를 인코딩한다. 행렬 표현에서 최솟값과 덧셈 연산이 형식식의 덧셈과 곱셈에 대응되며, 각 일함수 값은 행렬의 k개 열의 행렬식과 같다. 요청 도착 시 기저 변환과 행 대체를 통해 표현이 업데이트된다. 분석은 원래 행렬 표현의 좌표 쌍으로 정의된 포텐셜 함수 기반의 상환 분석을 사용한다. 009 15:10 ▲ 143 · 댓글 78 Apple, AI 생성 이미지 구분하는 '검증 사진' 기술 공개 애플이 아이폰 18 Pro와 Pro Max에 'Apple Reference Image'라는 검증 사진 기술을 선택 옵션으로 도입했다. 보안 · Apple Reference Image: A New Approach for Verified Photography
Apple, AI 생성 이미지 구분하는 '검증 사진' 기술 공개 Key Point AI 이미지 생성 기술이 고도화되면서 진짜 사진과 조작된 이미지를 구분하기 어려워진 상황에서, 하드웨어 레벨 보안으로 사진의 진정성을 증명하는 새로운 표준을 제시한다.
핵심 요약
애플이 아이폰 18 Pro와 Pro Max에 'Apple Reference Image'라는 검증 사진 기술을 선택 옵션으로 도입했다. 이 기술은 카메라 센서가 정확히 포착한 이미지를 암호화된 타임스탬프와 함께 기록해 실제 촬영임을 증명한다. 센서 조작이나 소프트웨어 공격으로부터 보호하기 위해 하드웨어 레벨의 보안과 Private Cloud Compute를 활용한다. 이미지 내용은 애플을 포함한 누구도 볼 수 없으며, 위조 이미지 발견 시 촬영자의 신원 노출 없이 무효화할 수 있다. 기존 업계 표준(C2PA)과 달리 편집 과정의 모든 단계에서 손상될 수 있는 취약점을 해결하는 방식이다. 010 08:25 ▲ 244 · 댓글 151 신원 인증 업체 침해, 1억 5300만 건 미국 운전면허증 유출 다크웹 서비스 Nexus가 신원 인증 업체 IDScan에서 유출된 미국·캐나다 운전면허증 1억 5300만 건과 여행증명서 300만 건을 판매 중이다. 보안 · America's Driver's License Breach Is a National Security Disaster
신원 인증 업체 침해, 1억 5300만 건 미국 운전면허증 유출 Key Point 국방·정보 기관과 일반인의 신원 정보가 적국 정보기관에 악용될 수 있는 국가 안보 위협이기 때문이다.
핵심 요약
다크웹 서비스 Nexus가 신원 인증 업체 IDScan에서 유출된 미국·캐나다 운전면허증 1억 5300만 건과 여행증명서 300만 건을 판매 중이다. Nexus는 1년 이상 지속적으로 데이터를 탈취했으며, 하루 약 40만 건씩 새로운 데이터가 유입되고 있다. 미국 정부 고위 인사들의 면허증도 포함되어 있으며, 기술 기자 Brian Krebs가 자신과 친인척 9명의 진정성 있는 면허증을 확인했다. 운전면허증은 신원 도용과 피싱 공격에 사용될 뿐 아니라, 중국·러시아 같은 적국의 정보기관이 다른 데이터베이스와 연결해 미국 첩보망을 추적하는 데 활용될 수 있다. 2010년대 중반 중국 해킹 그룹들이 탈취한 Anthem·Equifax·marriott 데이터가 미국 정보 활동 대응에 사용된 전례가 있다. 신원 인증 업체들의 유출 사건이 빈번한 만큼, 규제와 감시 강화 필요성이 제기되고 있다. 011 08:25 ▲ 750 · 댓글 275 9·11 이후 25년, 대규모 감시 체계 점검의 시간 9·11 이후 정부는 테러 대응이라는 명목으로 개인 도청에서 인터넷 백본 감시, 메타데이터 대량 수집 같은 대규모 감시 체계로 전환했다. 보안 · 25 years of mass surveillance is enough
9·11 이후 25년, 대규모 감시 체계 점검의 시간 Key Point 25년간 이어진 대규모 감시 체계의 실효성이 증명되지 않은 상황에서 국민의 자유와 프라이버시 비용을 본격적으로 따져야 할 시점이기 때문이다.
핵심 요약
9·11 이후 정부는 테러 대응이라는 명목으로 개인 도청에서 인터넷 백본 감시, 메타데이터 대량 수집 같은 대규모 감시 체계로 전환했다. 현재 대규모 감시는 법집행 기관의 일상적 도구가 되었으며, ICE의 이민 단속, 경찰의 지능형 신호등 수집, 안면인식 카메라 등 광범위하게 사용 중이다. 민간 기업들의 감시는 구글·페이스북 같은 광고 기반 수익 모델에서 비롯되며, 통신사와 데이터 브로커를 통해 정부와 법집행기관에 정보가 흘러들어간다. FBI는 데이터 브로커로부터 미국인 정보를 구매하고 있으며, AI 기술의 발전으로 감시 능력과 그에 따른 문제가 동시에 확대되고 있다. 정부는 대규모 감시 프로그램의 비용·편익을 종합 분석한 적 없으며, 테러 방지 효과도 입증하지 못했다. 2013년 스노든 폭로로 2015년 미국 항소법원이 전화기록 대량 수집을 위헌으로 판단했고 같은 해 USA 프리덤법이 통과했지만, NSA의 Upstream 프로그램 등 대규모 감시는 계속되고 있다. 012 08:27 ▲ 207 · 댓글 297 상상도 못 하는 뇌 연구, 기존 시각 이론 뒤집다 정신 이미지가 뇌 한곳에서만 만들어진다는 기존 학설을 신경과학 논문이 반박했다. 기타 · People who can't picture anything are rewriting the science of imagination
상상도 못 하는 뇌 연구, 기존 시각 이론 뒤집다 Key Point 뇌에서 상상이 어떻게 작동하는지에 대한 기본 가정이 뒤흔들리는 중이며, 심상 불능증처럼 과학이 주목하지 않던 조건이 뇌 작동의 핵심 메커니즘을 밝히는 열쇠가 되고 있다.
핵심 요약
정신 이미지가 뇌 한곳에서만 만들어진다는 기존 학설을 신경과학 논문이 반박했다. 시각 피질이 심각하게 손상되어도 상상할 수 있는 환자들과 아판타시아(심상 불능증) 사례가 이를 증명한다. 뇌 스캔 분석 결과 상상은 전두엽과 좌측 측두엽 융합 회선 같은 여러 지역이 협력해 만드는 현상이다. 심상 불능증 환자들은 내적 이미지가 없어도 공간 정보 인식을 통해 테트리스 같은 작업을 수행할 수 있다. 약한 전기 자극으로 시각 피질을 억제하면 오히려 심상이 더 생생해지는 현상도 기존 이론과 모순된다. 013 06:10 ▲ 175 · 댓글 37 분산 시스템의 고전 논문 10편을 한곳에 분산 시스템 연구를 주도한 영향력 있는 논문들을 선별한 리스트입니다. 인프라 · 데브옵스 · Distributed Systems Classics (2017)
분산 시스템의 고전 논문 10편을 한곳에 Key Point 분산 시스템을 깊이 있게 학습하려는 개발자와 연구자가 핵심 논문 10편을 체계적으로 접근할 수 있는 로드맵을 제공합니다.
핵심 요약
분산 시스템 연구를 주도한 영향력 있는 논문들을 선별한 리스트입니다. Lamport의 논리적 시계, 비잔틴 장군 문제, 분산 스냅샷부터 합의 불가능성 증명, Paxos, Bitcoin, CRDT, Raft까지 포함됩니다. 각 논문은 DOI나 원문 링크와 함께 연도별로 정렬되어 1978년부터 2014년까지의 이론적 기초를 제시합니다. 014 06:10 ▲ 121 · 댓글 48 AI 수학 자동화 시대, 인간 수학자의 역할 재정의해야 AI 시스템이 IMO 수준의 수학 문제 해결과 난제 자동 해결에 성공하면서 수학 분야의 급격한 변화가 진행 중이다. AI · 머신러닝 · A Beginning for Mathematics
AI 수학 자동화 시대, 인간 수학자의 역할 재정의해야 Key Point 수학자들이 AI의 정리 증명 능력을 보고 느끼는 위기감이 사실은 직업 보호의 신호가 아니라, 수학의 진정한 목표가 무엇인지 재정의하는 기회를 제시한다.
핵심 요약
AI 시스템이 IMO 수준의 수학 문제 해결과 난제 자동 해결에 성공하면서 수학 분야의 급격한 변화가 진행 중이다. 현재 수학 공동체는 정리 증명을 중심으로 가치를 평가해왔으나, AI가 자동으로 증명을 생산할 수 있게 되면 이 기준은 더 이상 유효하지 않다. 초인적 수준의 AI 수학 능력이 등장해도 개별 결과에 대한 인간의 이해(human understanding)는 자동으로 생기지 않으며, 이것이 인간 수학자의 필수적 역할이다. 학습 세미나, 우연한 대화, 공동체 학습 같은 현재의 학술 제도 형태는 보존하되, 그 안의 가치(understanding, 질문 제기, 설명력)에 집중해야 한다. 저널, 동료 심사, arXiv 같은 기존 제도의 형태를 보호하려는 시도는 현실적이지 않으며, 새로운 균형점을 찾아야 한다. 015 21:11 당일 +122 백그라운드 코딩 에이전트 오픈소스 공개 Ramp의 Inspect에서 영감을 받은 오픈소스 백그라운드 에이전트 시스템 Open-Inspect를 공개했다. AI · 머신러닝 · ColeMurray/background-agents · TypeScript
백그라운드 코딩 에이전트 오픈소스 공개 Key Point 백그라운드에서 자동으로 코드 작업을 처리해주는 AI 에이전트 시스템의 구체적인 구현 방식과 다양한 통합 옵션을 제시한다.
핵심 요약
Ramp의 Inspect에서 영감을 받은 오픈소스 백그라운드 에이전트 시스템 Open-Inspect를 공개했다. Node.js, Python, 브라우저 자동화 등 완전한 개발 환경에 접근하며 웹 UI, Slack, GitHub PR, Linear 이슈, 웹훅 등 여러 채널에서 작업을 요청할 수 있다. 여러 사용자가 실시간으로 협업하고 병렬 서브태스크를 실행하며 GitHub PR을 생성할 수 있으며, Claude, ChatGPT, Grok 등 다양한 AI 모델을 선택해 사용한다. 단일 테넌트 배포만 지원하며 조직 내 신뢰할 수 있는 모든 사용자가 같은 GitHub App 자격증명을 공유한다. Session은 파일시스템 스냅샷과 사전 빌드된 이미지로 빠르게 시작되며, 한 번의 세션에서 최대 10개 저장소를 함께 작업할 수 있다. 016 21:11 ▲ 102 · 댓글 83 AI가 나비에-스토크스 문제를 풀었다는 것의 의미 OpenAI는 2026년 9월 밀레니엄 상금 문제 중 하나인 나비에-스토크스 존재성과 정칙성 문제의 해를 제시했다고 발표했다. AI · 머신러닝 · After Math
AI가 나비에-스토크스 문제를 풀었다는 것의 의미 Key Point 형식적으로 증명되었다고 해서 수학의 진정한 진전이 이루어지는지, AI 시대 수학의 역할이 어떻게 재정의되어야 하는지를 다루는 근본적인 질문이기 때문이다.
핵심 요약
OpenAI는 2026년 9월 밀레니엄 상금 문제 중 하나인 나비에-스토크스 존재성과 정칙성 문제의 해를 제시했다고 발표했다. AI가 제출한 것은 Lean 형식 증명과 비형식 증명 원고인데, 이는 논리적 증명(기계적 검증 가능)의 기준은 충족하지만 수학자가 원하는 이해 가능한 증명은 아닐 수 있다. 논리적 증명과 이해 가능한 증명은 역사적으로 함께 진행되었으나, AI로 인해 형식 증명만 남고 수학적 통찰력 없는 증명이 생겨날 수 있다. 수학은 문제 해결만이 아니라 새로운 개념 개발, 이론 구축, 질문 제기, 커뮤니티 형성, 아름다움 추구 등 훨씬 광범위한 활동이다. AI가 수학 문제를 '해결했다'는 서사는 수학이 단순히 문제 풀이이며 형식적 답만 중요하다는 두 가지 잘못된 가정에 기반한다. 017 12:10 ▲ 101 · 댓글 48 25년 후 9·11 피해자들, 암·중피종으로 계속 죽어간다 뉴욕 흉부외과의사는 그라운드 제로 근처에 있었던 사람들이 25년 뒤인 지금도 폐암, 식도암, 중피종 등으로 고통받고 있다고 증언한다. 기타 · New York thoracic surgeon: "For many patients 9/11 is not over"
25년 후 9·11 피해자들, 암·중피종으로 계속 죽어간다 Key Point 9·11 테러의 장기적 건강 영향이 여전히 수만 명에게 진행 중이며, 의료계가 처리해야 할 현실적 과제임을 보여준다.
핵심 요약
뉴욕 흉부외과의사는 그라운드 제로 근처에 있었던 사람들이 25년 뒤인 지금도 폐암, 식도암, 중피종 등으로 고통받고 있다고 증언한다. 콘크리트 분진, 석면, 중금속, 연소 생성물이 포함된 폐허의 먼지를 마신 응급 대응자, 건설 노동자, 주민들이 질병을 앓고 있다. 14만 명 이상의 피해자가 연방 관리 9·11 건강 프로그램에 등록되어 있으며, 수만 명이 암, 호흡기 질환, 소화기 질환을 진단받았다. 의학적으로 개인 환자의 암이 그라운드 제로 노출로 인한 것임을 확실히 증명할 수 없지만, 역학 조사는 노출 인구에서 질병 발생률이 높음을 보여준다. 018 06:10 ▲ 114 · 댓글 37 NSA 대량감시 시설 '641A' - AT&T 고발에서 합법화까지 2003년부터 샌프란시스코 AT&T 건물에서 NSA가 운영해온 Room 641A는 광통신 인터넷 트래픽을 대규모로 가로채 감시하는 시설이다. 보안 · Room 641A
NSA 대량감시 시설 '641A' - AT&T 고발에서 합법화까지 Key Point 미국 국가보안국의 광범위한 대량감시 체계가 실제로 어떻게 작동했으며, 법적 투명성과 국가 안보의 충돌에서 국가권력이 어떻게 '합법화'되는지 보여주는 역사적 사례.
핵심 요약
2003년부터 샌프란시스코 AT&T 건물에서 NSA가 운영해온 Room 641A는 광통신 인터넷 트래픽을 대규모로 가로채 감시하는 시설이다. 2006년 AT&T 기술자 마크 클라인이 존재를 공개했고, 전자프론티어재단(EFF)이 불법 감시 혐의로 소송을 제기했다. 클라인은 미국 전역에 유사한 '검은 방'이 운영되고 있다고 주장했다. 법원은 수년간의 소송 끝에 2011년 의회가 협력 통신사에 소급 면책권을 부여하면서 소송이 기각됐다. 2019년 최종 판결에서 법원은 클라인이 시설의 실제 운영 내용을 증명할 수 없다고 결론지었다. 019 09:10 ▲ 125 · 댓글 121 OpenAI, Navier-Stokes 증명을 Lean 4 형식 증명으로 공개 OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다. AI · 머신러닝 · OpenAI’s Navier-Stokes release included a Lean 4 formal proof
OpenAI, Navier-Stokes 증명을 Lean 4 형식 증명으로 공개 Key Point 형식 검증 비용이 만 배 절감되면서 AI 증명 방식이 학문과 산업 전반의 검증 방식을 근본적으로 바꿀 수 있는 전환점이 되었다.
핵심 요약
OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다. 종전에는 수학 논문 한 페이지를 형식화하는 데 약 40시간이 소요되었으나, 이번 증명은 17시간 만에 Lean 형식으로 검증되었다. 166쪽 규모의 OpenAI 논문을 전통적 방식으로 형식화했다면 13만 2800인시가 필요했을 것으로 추정되어, 약 만 배의 비용 감소를 의미한다. 형식 증명의 비용이 급격히 낮아지면서 수학 연구뿐 아니라 보안 정책 검증, 스마트 계약 검증, 미션 크리티컬 알고리즘 검증 등이 현실화될 수 있다. 020 09:10 ▲ 251 · 댓글 260 애플, 가변 조리개 카메라 탑재한 아이폰 18 프로 공개 애플이 아이폰 18 프로와 프로 맥스를 발표했으며, 48MP 퓨전 메인 카메라에 가변 조리개를 처음 도입했다. 하드웨어 · 시스템 · iPhone 18 Pro and iPhone 18 Pro Max
애플, 가변 조리개 카메라 탑재한 아이폰 18 프로 공개 Key Point 가변 조리개는 스마트폰 카메라의 창의적 제어를 근본적으로 바꾸는 기술이며, 참조 이미지로 사진 진위 확인이 가능해지는 것은 콘텐츠 신뢰성 측면에서 중요한 변화다.
핵심 요약
애플이 아이폰 18 프로와 프로 맥스를 발표했으며, 48MP 퓨전 메인 카메라에 가변 조리개를 처음 도입했다. 조리개는 6개의 레이저 커팅 블레이드로 f/1.48부터 f/4까지 자동 또는 수동으로 조절되어 저조도 촬영과 깊이감 제어가 가능하다. 새로운 센서와 연산 이미징 파이프라인으로 더 선명한 사진을 생성하며, 촬영 후 시네마틱 효과 적용, 4K 돌비 비전 HDR 타임랩스 등을 지원한다. 프로 컨트롤 기능으로 사용자가 조리개, 셔터 스피드, 화이트 밸런스를 수동으로 조정할 수 있고, 히스토그램 확인도 가능하다. A20 프로 칩과 신형 베이퍼 챔버로 아이폰 역사상 최고의 지속 성능을 제공하며, 프로 맥스는 배터리 용량 증가로 아이폰 최대 수준의 배터리 개선을 달성했다. 애플 레퍼런스 이미지 기능으로 메인 카메라의 센서가 모든 픽셀에 서명하여 사진의 진위 여부와 편집 여부를 증명할 수 있다. 021 11:10 ▲ 216 · 댓글 48 태양계 얼음 달들은 거대한 물의 세계 과학 이해의 발전으로 태양계 외곽의 얼음 달들이 단순한 얼음 천체에서 지하 바다를 품은 물의 세계로 재평가됐다. 하드웨어 · 시스템 · Icy Moons Are Ocean Worlds
태양계 얼음 달들은 거대한 물의 세계 Key Point 태양계 내 생명 탐사의 중심지가 어디인지, 그리고 우리가 어떤 증거들로 이 얼음 달들을 재평가하게 됐는지를 보여주는 과학 발전의 흐름을 담고 있다.
핵심 요약
과학 이해의 발전으로 태양계 외곽의 얼음 달들이 단순한 얼음 천체에서 지하 바다를 품은 물의 세계로 재평가됐다. 보이저, 갈릴레오, 카시니 탐사선과 우주 망원경 관측을 통해 유로파, 엔셀라두스, 타이탄, 미마스, 칼리스토, 가니메데 6개 달에서 대규모 지하 액체 수역이 확인됐다. 목성의 위성 유로파는 자기장 증거로 2000년 지하 바다의 존재가 증명된 첫 번째 후보였으며, 방사선으로 생성된 산소와 과산화물이 바다로 순환할 가능성이 있다. 목성 위성 가니메데는 태양계 최대 규모의 바다를 보유했으며 100마일 이상의 얼음층 아래 숨겨져 있고, 허블 우주 망원경의 극광 관측으로 2011년 전 지구적 바다의 존재가 확인됐다. 토성의 위성 엔셀라두스는 남반구의 호랑이 줄무늬에서 우주로 거대한 바닷물 기둥을 분출하며, 2008년 카시니 탐사선이 이 분출물을 직접 샘플링해 생명 존재 가능성을 높였다. 022 11:10 ▲ 134 · 댓글 140 AI가 증명한 수학 정리, 인간 수학자의 미래를 묻다 1974년 이래 미해결 난제였던 '구면 하드비거 정리'를 중국 연구팀이 OpenAI Codex의 도움을 받아 증명했다. AI · 머신러닝 · Is mathematics about to enter the conservatory?
AI가 증명한 수학 정리, 인간 수학자의 미래를 묻다 Key Point AI가 순수수학의 최고 난제까지 해결하기 시작하면서, 수학 연구의 가치와 수학자 직업의 미래에 대한 근본적 질문이 제기되고 있습니다.
핵심 요약
1974년 이래 미해결 난제였던 '구면 하드비거 정리'를 중국 연구팀이 OpenAI Codex의 도움을 받아 증명했다. AI는 증명 세부사항 개발, 틈새 발견·보완, 논문 작성과 편집 등 기존에 연구 수학자만 가능하던 작업을 수행했다. OpenAI는 GPT-4 출시 시 LLM 노출도 분석에서 수학자 직업의 100%가 자동화 위험에 처해있다고 보고했으며, 다른 창작 분야보다 영향이 가장 크다. 저자는 클래식 음악이 보존되는 방식처럼 순수수학도 대학과 문화기관 중심의 '수학 음악원' 모델로 재편성될 수 있다고 제안한다. 현 재정 지원 체계는 AI 시대에 맞지 않으며, 인간 수학자가 가치 있는 이유를 재정의하고 지원 방식을 급진적으로 변화시켜야 한다고 주장한다. 023 08:12 ▲ 358 · 댓글 200 웹어셈블리로 보트 차단, 1년 개발한 Anubis AI 업체의 공격적인 웹 스크래핑으로부터 서버를 보호하기 위해 Anubis라는 도구를 개발했다. 보안 · It took a year to ship WebAssembly in Anubis
웹어셈블리로 보트 차단, 1년 개발한 Anubis Key Point 웹사이트 다운타임을 야기하는 AI 스크래핑 문제에 대한 기술적 대응 방식을 보여주며, 개별 사용자 경험과 대규모 악의적 접근을 구분하는 새로운 접근법을 제시합니다.
핵심 요약
AI 업체의 공격적인 웹 스크래핑으로부터 서버를 보호하기 위해 Anubis라는 도구를 개발했다. 해시캐시 방식의 작업증명(PoW) 챌린지를 사용해 개별 사용자에게는 무시할 수 있는 수준의 부하를 주지만, 대규모 스크래퍼에게는 비용을 크게 증가시킨다. 현재는 임시 해결책이며, 향후 헤드리스 브라우저를 탐지해 정상 사용자에게는 챌린지를 표시하지 않을 계획이다. 최신 자바스크립트 기능을 사용하므로 JShelter 같은 보안 플러그인을 비활성화해야 한다. 024 08:12 ▲ 266 · 댓글 95 AI가 풀어낸 40년 난제들, 수학 해커톤에서 새로운 가설에 도전 칼텍이 10월 30일부터 11월 1일까지 최초의 연구급 수학 해커톤 'Mathathon'을 개최한다. AI · 머신러닝 · Caltech Mathathon – first hackathon ever devoted to research level mathematics
AI가 풀어낸 40년 난제들, 수학 해커톤에서 새로운 가설에 도전 Key Point AI가 기초 수학 문제를 풀기 시작한 가운데, 수학자의 역할과 AI 활용의 미래 방향을 현장에서 직접 탐색하는 첫 시도이기 때문이다.
핵심 요약
칼텍이 10월 30일부터 11월 1일까지 최초의 연구급 수학 해커톤 'Mathathon'을 개최한다. 100개 팀이 40시간 동안 최신 AI 모델을 활용해 미해결 난제를 풀고 새로운 수학 이론을 구축한다. 올해 AI가 80년, 78년, 27년 된 3개의 주요 추측을 증명·반증한 사례들이 수학계를 자극했다. 참가팀은 수백만 달러 규모의 AI 크레딧을 지원받으며, 결과물을 수학자 심사위원단 앞에서 방어해야 한다. 현장 심사와 별개로 수학계의 검증 이후 2차 시상식을 진행하며 우수한 결과에 상금을 지급한다. 025 20:31 ▲ 178 · 댓글 76 러셀과 화이트헤드의 '수학 원리', 현대 논리학의 뿌리를 찾다 '수학 원리'는 기본 공리만으로 모든 수학이 유도 가능함을 보이기 위해 극도로 상세한 증명을 제시했다. 기타 · Principia Mathematica is modern and insightful
러셀과 화이트헤드의 '수학 원리', 현대 논리학의 뿌리를 찾다 Key Point 수학 기초론의 고전 저작이 현대 논리학과 형식 체계에 끼친 영향을 학술적으로 분석한 글로, 개발자와 이론 전산학자들 사이에서 역사적 통찰력을 찾는 독자들로부터 주목받고 있다.
핵심 요약
'수학 원리'는 기본 공리만으로 모든 수학이 유도 가능함을 보이기 위해 극도로 상세한 증명을 제시했다. 한때 '명백한 변수'로 부르던 개념은 현대의 한정변수(bound variable)이며, 람다 계산법의 역사적 기원을 보여준다. '수학 원리'는 1910년에 벌써 '정확한 기술'과 '명시적 함수'의 차이를 구분했으며, 수학의 함수적 과정들을 분류했다. 
