diff --git a/client/public/locales/ko/.gitignore b/client/public/locales/ko/.gitignore
new file mode 100644
index 0000000..4ffa873
--- /dev/null
+++ b/client/public/locales/ko/.gitignore
@@ -0,0 +1,8 @@
+/ko-level1.tmx
+/ko-level2.tmx
+/ko-omegat.tmx
+/**/*.bak
+/omegat/last_entry.properties
+/omegat/files_order.txt
+/omegat/project_stats.txt
+/tm/*.tmx
diff --git a/client/public/locales/ko/README.ko.md b/client/public/locales/ko/README.ko.md
new file mode 100644
index 0000000..98760d5
--- /dev/null
+++ b/client/public/locales/ko/README.ko.md
@@ -0,0 +1,15 @@
+# 린 4 게임
+
+[English (영어)](./README.md) | 한국어
+
+## 기여하기
+
+`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
+
+### 한국어 번역
+
+저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
+
+[bc]: https://github.com/chabulhwi
+[omt]: https://omegat.org/
+[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
diff --git a/client/public/locales/ko/README.md b/client/public/locales/ko/README.md
new file mode 100644
index 0000000..4ad9c9b
--- /dev/null
+++ b/client/public/locales/ko/README.md
@@ -0,0 +1,18 @@
+# Lean 4 Game
+
+English | [한국어[Korean]](./README.ko.md)
+
+## Contributing
+
+Contributions to the Korean translation of `lean4game` are always welcome!
+
+### Korean Translation
+
+I ([Bulhwi Cha][bc]) use [OmegaT][omt] to translate English documentation into
+Korean. The OmegaT project is in this directory, that is,
+`client/public/locales/ko`. You need to install the [Okapi filters plugin for
+OmegaT][okapi] to make OmegaT parse JSON files.
+
+[bc]: https://github.com/chabulhwi
+[omt]: https://omegat.org/
+[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
diff --git a/client/public/locales/ko/dictionary/.gitignore b/client/public/locales/ko/dictionary/.gitignore
new file mode 100644
index 0000000..e69de29
diff --git a/client/public/locales/ko/glossary/glossary.txt b/client/public/locales/ko/glossary/glossary.txt
new file mode 100644
index 0000000..130f339
--- /dev/null
+++ b/client/public/locales/ko/glossary/glossary.txt
@@ -0,0 +1,167 @@
+# Glossary in tab-separated format -*- coding: utf-8 -*-
+St. Anselm 안셀무스
+ontological 존재론적
+argument 논증
+argument 인수
+Lean 린
+Lean community 린 커뮤니티
+God 신
+Alvin Plantinga 앨빈 플랜팅아
+exist 존재하다
+existence 존재
+the understanding 지성
+reality 현실
+assumption 가정
+reductio 귀류법
+great 큰
+premise 전제
+being 존재자
+conceive 생각하다
+definition 정의
+true 참
+true 참인
+false 거짓
+false 거짓인
+formulate 정식화하다
+formulation 정식화
+formalize 형식화하다
+formalization 형식화
+property 속성
+redundant 불필요한
+sentence 문장
+state 진술하다
+statement 진술
+proposition 명제
+negation 부정
+axiom 공리
+theorem 정리
+theory 이론
+conclude 결론하다
+prove 증명하다
+SEP 스탠퍼드 철학 백과사전
+Eric Wieser 에릭 비저
+Alistair Tucker 앨리스터 터커
+philosophy 철학
+Owl of Sogang 서강올빼미
+type theory 유형론
+universe level 유형 세계 변수
+type 유형
+type 입력하다
+type check 유형을 확인하다
+type check 유형이 확인되다
+type check 유형 확인이 잘되다
+type class 유형 클래스
+instance 사례
+category mistake 범주 실수
+class 클래스
+example 보기
+example 예
+inductive type 귀납형
+define 정의하다
+constructor 구성자
+Apache License, Version 2.0 아파치 라이선스, 버전 2.0
+under the terms of 의 조건에 따라
+OmegaT 오메가T
+symbolic link 심벌릭 링크
+directory 디렉터리
+root directory 최상위 디렉터리
+documentation 문서
+English 영어
+Korean 한국어
+chapter 장
+quiz 퀴즈
+question 문제
+command 명령어
+error 오류
+code 코드
+evaluate 계산하다
+keyword 핵심어
+declare 선언하다
+constant 상수
+reference 참고 문헌
+universe-polymorphic 세계 다형적
+parametrically polymorphic 매개 변수 다형적
+function 함수
+identifier 식별자
+definitionally equal 정의상 같은
+natural number 자연수
+input 입력값
+return 반환하다
+non-zero 영이 아닌
+zero 영
+alpha-equivalent 알파 동등한
+less-than-or-equal-to sign 작거나 같음 부호
+dependent function 의존 함수
+dependent function type 의존 함수형
+dependent product 의존곱
+dependent product type 의존곱형
+underscore 밑줄
+implicit 암시적
+explicit 명시적
+sigma type 시그마
+propositional logic 명제 논리
+term 항
+contemporary 동시대
+term 용어
+truth-value 진릿값
+bearer 담지자
+propositional attitudes 명제적 태도
+believe 믿다
+doubt 의심하다
+South Korea 한국
+school mathematics 학교 수학
+sentence 문장
+high school mathematics 고등학교 수학
+teacher 교사
+Stanford Encyclopedia of Philosophy 스탠퍼드 철학 백과사전
+ordered triple 순서세짝
+conjecture 추측
+Goldbach's conjecture 골드바흐의 추측
+interactive theorem prover 상호 작용 정리 증명기
+truth 참
+falsity 거짓
+rule of inference 추론 규칙
+introduction rule 도입 규칙
+elimination rule 제거 규칙
+ex falso quodlibet 엑스 팔소 세퀴투르 쿠오들리베트
+principle of explosion 폭발 원리
+propositional connective 명제 연결사
+symbol 기호
+refutation by contradiction 모순에 따른 부인
+contradiction 모순
+conjunction 연언
+disjunction 선언(選言)
+implication 함의
+material implication 내용적 함의
+conditional 조건문
+modus ponens 긍정 논법[모더스 포넨스]
+necessary condition 필요조건
+conversion 역
+inversion 이(裏)
+contraposition 대우(對偶)
+equivalence 동등
+biconditional 쌍조건문
+abbreviation 준말
+if and only if …일 때 그리고 그럴 때만
+editor 편집기
+shortcut 단축키
+Theorem Proving in Lean 4 린 4로 하는 정리 증명
+exercise 연습 문제
+repository 저장소
+Jeremy Avigad 제러미 아비가드
+Leonardo de Moura 레오나르두 지 모라
+Soonho Kong 공순호
+Sebastian Ullrich 제바스티안 울리히
+file 파일
+Markdown 마크다운
+quiz 퀴즈
+translation 번역
+contribute 기여하다
+progress 진도
+capacity 이용량
+GitHub 깃허브
+repo 저장소
+game rule 게임 규칙
+unlocked 잠금 해제가 된
+unlock 잠금 해제를 하다
+Markdown 마크다운
diff --git a/client/public/locales/ko/omegat.project b/client/public/locales/ko/omegat.project
new file mode 100644
index 0000000..34cc557
--- /dev/null
+++ b/client/public/locales/ko/omegat.project
@@ -0,0 +1,33 @@
+
+
+
+ __DEFAULT__
+
+ **/.svn/**
+ **/CVS/**
+ **/.cvs/**
+ **/.git/**
+ **/.hg/**
+ **/.repositories/**
+ **/desktop.ini
+ **/Thumbs.db
+ **/.DS_Store
+ **/~$*
+
+ __DEFAULT__
+ __DEFAULT__
+ __DEFAULT__
+ __DEFAULT__
+ __DEFAULT__
+ __DEFAULT__
+ omegat level1 level2
+ en
+ ko
+ org.omegat.tokenizer.LuceneEnglishTokenizer
+ org.omegat.tokenizer.HunspellTokenizer
+ true
+ true
+ false
+
+
+
diff --git a/client/public/locales/ko/omegat/ignored_words.txt b/client/public/locales/ko/omegat/ignored_words.txt
new file mode 100644
index 0000000..e69de29
diff --git a/client/public/locales/ko/omegat/learned_words.txt b/client/public/locales/ko/omegat/learned_words.txt
new file mode 100644
index 0000000..e69de29
diff --git a/client/public/locales/ko/omegat/project_save.tmx b/client/public/locales/ko/omegat/project_save.tmx
new file mode 100644
index 0000000..05006e6
--- /dev/null
+++ b/client/public/locales/ko/omegat/project_save.tmx
@@ -0,0 +1,1009 @@
+
+
+
+
+
+
+
+
+ <0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL.
+
+
+ <0>여러분이 직접 게임을 작성할 생각이 있다면, <1>GameSkeleton 깃허브 저장소</1>를 양식[템플릿]으로 이용하고 <3>'게임 만들기(Creating a Game)'</3> 문서를 읽으십시오.</0><1>여러분이 작성한 게임을 직접 서버에서 불러오고, 정확한 URL을 이용해 그 게임을 하실 수 있습니다.
+
+
+
+
+ <p>As this server runs lean on our university machines, it has a limited capacity.
+
+
+ <p>이 서버는 저희 대학의 여러 컴퓨터에서 린을 실행하므로 그 이용량이 제한돼 있습니다.
+
+
+
+
+ <p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory.
+
+
+ <p>저장된 진도를 불가역적으로 삭제하시겠습니까?</p><p>(이를 선택하시면 증명과 인벤토리 안의 수집 항목들이 삭제됩니다.
+
+
+
+
+ <p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level.
+
+
+ <p>게임 규칙에 따라, 단계들을 건너뛰어도 되는지 그리고 증명을 작성할 때 잠금 해제가 된 전략과 정리만 이용할 수 있는지가 정해집니다.</p><1>
+
+참고: '잠금 해제'가 된 전략이나 정리는 다음 두 부류로 정해집니다. (1) 해당 단계를 푸는 데 필요한 최소한의 전략이나 정리의 모임, (2) 다른 단계에서 잠금 해제를 한 전략이나 정리.
+
+
+
+
+ <p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress!
+
+
+ <p>저장된 게임 진도가 있는 JSON 파일을 선택해 진도를 불러오십시오.</p><1><0>경고:</0> 이를 실행하면 현재의 게임 진도가 삭제됩니다!
+
+
+
+
+ A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>
+
+
+ <1>린(Lean 4)</1> 증명 보조기와 그 수학 라이브러리 <5>매스리브(mathlib)</5>를 학습하기 위한 게임들의 저장소
+
+
+
+
+ Active Goal
+
+
+ 활성화된 목표
+
+
+
+
+ Adding new games
+
+
+ 새 게임 추가하기
+
+
+
+
+ Always visible
+
+
+ 항상 보임
+
+
+
+
+ Assumptions
+
+
+ 가정
+
+
+
+
+ Auto
+
+
+ 자동
+
+
+
+
+ CPU
+
+
+ CPU
+
+
+
+
+ Cancel
+
+
+ 취소하기
+
+
+
+
+ Character
+
+
+ 문자
+
+
+
+
+ Clear Progress
+
+
+ 진도 없애기
+
+
+
+
+ Click somewhere in the Lean file to enable the infoview.
+
+
+ 린 파일의 아무 곳이나 눌러 정보창을 여십시오.
+
+
+
+
+ Consider <2>downloading your current progress</2> first!</1>
+
+
+ <2>현재의 게임 진도</2>를 먼저 내려받을지 판단하십시오!</1>
+
+
+
+
+ Contributing
+
+
+ 기여하기
+
+
+
+
+ Contributions to the Korean translation of <g1>lean4game</g1> are always welcome!
+
+
+ <g1>lean4game</g1>의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
+
+
+
+
+ Crashed!
+
+
+ 시스템 다운됨!
+
+
+
+
+ Current Goal
+
+
+ 현재 목표
+
+
+
+
+ Definitions
+
+
+ 정의
+
+
+
+
+ Delete
+
+
+ 삭제하기
+
+
+
+
+ Delete Progress?
+
+
+ 진도를 삭제하시겠습니까?
+
+
+
+
+ Desktop
+
+
+ 데스크톱
+
+
+
+
+ Development notes
+
+
+ 개발 노트
+
+
+
+
+ Download
+
+
+ 내려받기
+
+
+
+
+ Download & Delete
+
+
+ 내려받고 삭제하기
+
+
+
+
+ Download Progress
+
+
+ 진도 내려받기
+
+
+
+
+ Editor mode
+
+
+ 편집기 모드
+
+
+
+
+ Editor mode is enforced!
+
+
+ 편집기 모드가 강제됐습니다!
+
+
+
+
+ English | <g1>한국어[Korean]</g1>
+
+
+ [English (영어)](./README.md) | 한국어
+
+
+
+
+ Erase
+
+
+ 지우기
+
+
+
+
+ Execute
+
+
+ 실행하기
+
+
+
+
+ Failed command
+
+
+ 실패한 명령
+
+
+
+
+ Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>
+
+
+ 문제를 겪으면 거리낌 없이 <1>깃허브 이슈</1>를 제출해 주세요!</1>
+
+
+
+
+ Funding
+
+
+ 재정 지원
+
+
+
+
+ Further Goals
+
+
+ 이후 목표
+
+
+
+
+ Game Info
+
+
+ 게임 정보
+
+
+
+
+ Game Info & Credits
+
+
+ 게임 정보 및 제작자 명단
+
+
+
+
+ Game Introduction
+
+
+ 게임 소개
+
+
+
+
+ Game Rules
+
+
+ 게임 규칙
+
+
+
+
+ Go to editor mode and fix your proof!
+
+
+ 편집기 모드에서 증명을 고치십시오!
+
+
+
+
+ Goal
+
+
+ 목표
+
+
+
+
+ Home
+
+
+ 홈
+
+
+
+
+ I (<g1>Bulhwi Cha</g1><g2></g2><e8/>) use <g3>OmegaT</g3><g4></g4><e9/> to translate English documentation into
+Korean.
+
+
+ 저(<g1>차불휘</g1><g2></g2><e8/>)는 <g3>오메가T(OmegaT)</g3><g4></g4><e9/>를 이용해 영어 문서를 한국어로 번역합니다.
+
+
+
+
+ I (<g1>Bulhwi Cha</g1><g2></g2><e9/>) use <g3>OmegaT</g3><g4></g4><e10/> to translate English documentation into Korean.
+
+
+ 저(<g1>차불휘</g1><g2></g2><e9/>)는 <g3>오메가T(OmegaT)</g3><g4></g4><e10/>를 이용해 영어 문서를 한국어로 번역합니다.
+
+
+
+
+ Impressum
+
+
+ 관리자 정보
+
+
+
+
+ Intro
+
+
+ 소개
+
+
+
+
+ Introduction
+
+
+ 소개
+
+
+
+
+ Inventory
+
+
+ 인벤토리
+
+
+
+
+ Korean Translation
+
+
+ 한국어 번역
+
+
+
+
+ Language
+
+
+ 언어
+
+
+
+
+ Last server response:
+
+
+ 마지막 서버 응답:
+
+
+
+
+ Layout
+
+
+ 레이아웃
+
+
+
+
+ Lean 4 Game
+
+
+ 린 4 게임
+
+
+
+
+ Lean Game Server
+
+
+ 린 게임 서버
+
+
+
+
+ Leave World
+
+
+ 세계에서 나가기
+
+
+
+
+ Level
+
+
+ 단계
+
+
+
+
+ Level completed with warnings 🎭
+
+
+ 경고 있는 채로 단계 완료 🎭
+
+
+
+
+ Level completed!
+
+
+ 단계 완료!
+
+
+
+
+ Levels
+
+
+ 단계
+
+
+
+
+ Line
+
+
+ 줄
+
+
+
+
+ Load Progress from JSON
+
+
+ JSON에서 진도 불러오기
+
+
+
+
+ Load selected file
+
+
+ 선택한 파일 열기
+
+
+
+
+ Loading goal…
+
+
+ 목표 불러오는 중…
+
+
+
+
+ Loading messages…
+
+
+ 메시지 불러오는 중…
+
+
+
+
+ Mobile
+
+
+ 모바일
+
+
+
+
+ Next
+
+
+ 다음
+
+
+
+
+ No Games loaded.
+
+
+ 불러온 게임 없음.
+
+
+
+
+ No Goals
+
+
+ 목표 없음
+
+
+
+
+ Not available in this level
+
+
+ 이 단계에서 쓸 수 없음
+
+
+
+
+ Not unlocked yet
+
+
+ 아직 잠금 해제가 안 됨
+
+
+
+
+ Objects
+
+
+ 객체
+
+
+
+
+ Our current estimate is about 70 simultaneous games.
+
+
+ 현재 이 서버로 최대 70게임을 동시에 실행할 수 있는 것으로 추정됩니다.
+
+
+
+
+ Please get in contact and we'll happily add yours.</p>
+
+
+ 저희에게 연락하시면 여러분의 게임을 기꺼이 추가하겠습니다.
+
+
+
+
+ Preferences
+
+
+ 기본 설정
+
+
+
+
+ Prerequisites
+
+
+ 선행 요건
+
+
+
+
+ Previous
+
+
+ 이전
+
+
+
+
+ RAM
+
+
+ 램
+
+
+
+
+ Retry
+
+
+ 다시 시도하기
+
+
+
+
+ Retry proof from here
+
+
+ 여기부터 증명 다시 시도하기
+
+
+
+
+ Rules
+
+
+ 규칙
+
+
+
+
+ Save my settings (in the browser store)
+
+
+ (브라우저에) 설정 저장하기
+
+
+
+
+ Saves from other games are not deleted.)</p>
+
+
+ 다른 게임에 저장된 정보는 삭제되지 않습니다.)</p>
+
+
+
+
+ Server capacity
+
+
+ 서버 이용량
+
+
+
+
+ Show more help!
+
+
+ 도움말 더 보기!
+
+
+
+
+ Start
+
+
+ 시작하기
+
+
+
+
+ Tactics
+
+
+ 전략
+
+
+
+
+ That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>
+
+
+ 따라서 여러분이 <1>simp</1> 전략을 잠금 해제 하면, 그 뒤로 어느 단계에서든 이 전략을 이용할 수 있습니다.</1><p>선택할 수 있는 게임 규칙은 다음과 같습니다.</p>
+
+
+
+
+ The <1>instructions above</1> also explain the details for how to load your game to the server.
+
+
+ 여러분의 게임을 서버에서 불러오는 방법에 관한 세부 사항도 위의 <1>설명서</1>에 나와 있습니다.
+
+
+
+
+ The OmegaT project is in the <g5><g6>omegat</g6></g5> directory.
+
+
+ 오메가T 프로젝트는 <g5><g6>omegat</g6></g5> 디렉터리에 있습니다.
+
+
+
+
+ The OmegaT project is in this directory, that is,
+<g5>client/public/locales/ko</g5>.
+
+
+ 오메가T 프로젝트는 이 디렉터리, 다시 말해 <g5>client/public/locales/ko</g5>에 있습니다.
+
+
+
+
+ Theorems
+
+
+ 정리
+
+
+
+
+ This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.
+
+
+ 이 서버는 뒤셀도르프의 하인리히-하이네 대학에서 진행하는 <1>'아담(ADAM): 수학의 디지털 시대 준비하기'</1> 프로젝트의 일환으로 개발됐습니다.
+
+
+
+
+ Typewriter mode
+
+
+ 타자기 모드
+
+
+
+
+ Upload
+
+
+ 업로드
+
+
+
+
+ Upload Saved Progress
+
+
+ 저장된 진도 업로드
+
+
+
+
+ Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.
+
+
+ <1>http://localhost:3000/#/g/local/FOLDER</1>를 이용해 지역[로컬] 폴더에서 게임을 직접 여십시오.
+
+
+
+
+ Waiting for Lean server to start…
+
+
+ 린 서버가 시작하기를 기다리는 중…
+
+
+
+
+ We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development.
+
+
+ 미래에 저희가 서버 이용량 한계에 더 잘 대처하고 그 값을 보다 정확히 측정할 수 있기를 바랍니다.</p><1>게임과 그 기반 시설의 상당 부분은 여전히 개발 중입니다.
+
+
+
+
+ We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually.
+
+
+ 궁금한 점이 있으면 저희에게 연락해 주십시오.</1><p>이 페이지에 실린 게임들은 수동으로 추가됐습니다.
+
+
+
+
+ World
+
+
+ 세계
+
+
+
+
+ World selection
+
+
+ 세계 선택
+
+
+
+
+ Worlds
+
+
+ 세계
+
+
+
+
+ You need to install
+the <g7>Okapi filters plugin for OmegaT</g7><g8></g8><e11/> to make OmegaT parse Markdown
+files.
+
+
+ 오메가T로 마크다운 파일을 구문 분석 하려면 <g7>오메가T를 위한 오카피(Okapi) 필터 플러그인</g7><g8></g8><e11/>을 설치해야 됩니다.
+
+
+
+
+ You need to install the <g6>Okapi filters plugin for
+OmegaT</g6><g7></g7><e10/> to make OmegaT parse JSON files.
+
+
+ 오메가T로 JSON 파일을 구문 분석 하려면 <g6>오메가T를 위한 오카피(Okapi) 필터 플러그인</g6><g7></g7><e10/>을 설치해야 됩니다.
+
+
+
+
+ You need to install the <g6>Okapi filters plugin for
+OmegaT</g6><g7></g7><e10/> to make OmegaT parse Markdown files.
+
+
+ 오메가T로 마크다운 파일을 구문 분석 하려면 <g6>오메가T를 위한 오카피(Okapi) 필터 플러그인</g6><g7></g7><e10/>을 설치해야 됩니다.
+
+
+
+
+ back to games selection
+
+
+ 게임 선택하러 돌아가기
+
+
+
+
+ back to world selection
+
+
+ 세계 선택하러 돌아가기
+
+
+
+
+ close inventory
+
+
+ 인벤토리 닫기
+
+
+
+
+ information, Impressum, privacy policy
+
+
+ 정보, 관리자 정보, 사생활 정책
+
+
+
+
+ levels
+
+
+ 단계
+
+
+
+
+ next level
+
+
+ 다음 단계
+
+
+
+
+ none
+
+
+ 없음
+
+
+
+
+ previous level
+
+
+ 이전 단계
+
+
+
+
+ regular
+
+
+ 일반
+
+
+
+
+ relaxed
+
+
+ 완화됨
+
+
+
+
+ show inventory
+
+
+ 인벤토리 보기
+
+
+
+
+ tactics
+
+
+ 전략
+
+
+
+
+ used
+
+
+ 쓰임
+
+
+
+
+ view the Lean game server on GitHub
+
+
+ 깃허브에서 린 게임 서버 보기
+
+
+
+
+ view the Lean game server on Github
+
+
+ 깃허브에서 린 게임 서버 보기
+
+
+
+
+ 🎉
+
+
+ 🎉
+
+
+
+
+
diff --git a/client/public/locales/ko/source/README.md b/client/public/locales/ko/source/README.md
new file mode 120000
index 0000000..32d46ee
--- /dev/null
+++ b/client/public/locales/ko/source/README.md
@@ -0,0 +1 @@
+../README.md
\ No newline at end of file
diff --git a/client/public/locales/ko/source/translation.json b/client/public/locales/ko/source/translation.json
new file mode 120000
index 0000000..4a54b0f
--- /dev/null
+++ b/client/public/locales/ko/source/translation.json
@@ -0,0 +1 @@
+../../en/translation.json
\ No newline at end of file
diff --git a/client/public/locales/ko/target/README.md b/client/public/locales/ko/target/README.md
new file mode 100644
index 0000000..98760d5
--- /dev/null
+++ b/client/public/locales/ko/target/README.md
@@ -0,0 +1,15 @@
+# 린 4 게임
+
+[English (영어)](./README.md) | 한국어
+
+## 기여하기
+
+`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
+
+### 한국어 번역
+
+저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
+
+[bc]: https://github.com/chabulhwi
+[omt]: https://omegat.org/
+[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
diff --git a/client/public/locales/ko/target/translation.json b/client/public/locales/ko/target/translation.json
new file mode 100644
index 0000000..1906850
--- /dev/null
+++ b/client/public/locales/ko/target/translation.json
@@ -0,0 +1,98 @@
+{
+ "Tactics": "전략",
+ "Lean Game Server": "린 게임 서버",
+ "Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.
<1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp in a level, you can use it henceforth in any level.The options are:
": "게임 규칙에 따라, 단계들을 건너뛰어도 되는지 그리고 증명을 작성할 때 잠금 해제가 된 전략과 정리만 이용할 수 있는지가 정해집니다.<\/p><1>\n\n참고: '잠금 해제'가 된 전략이나 정리는 다음 두 부류로 정해집니다. (1) 해당 단계를 푸는 데 필요한 최소한의 전략이나 정리의 모임, (2) 다른 단계에서 잠금 해제를 한 전략이나 정리. 따라서 여러분이 <1>simp<\/1> 전략을 잠금 해제 하면, 그 뒤로 어느 단계에서든 이 전략을 이용할 수 있습니다.<\/1>
선택할 수 있는 게임 규칙은 다음과 같습니다.<\/p>",
+ "Game Rules": "게임 규칙",
+ "levels": "단계",
+ "tactics": "전략",
+ "regular": "일반",
+ "relaxed": "완화됨",
+ "none": "없음",
+ "Rules": "규칙",
+ "Intro": "소개",
+ "Game Introduction": "게임 소개",
+ "World selection": "세계 선택",
+ "Start": "시작하기",
+ "Inventory": "인벤토리",
+ "next level": "다음 단계",
+ "Next": "다음",
+ "back to world selection": "세계 선택하러 돌아가기",
+ "Leave World": "세계에서 나가기",
+ "previous level": "이전 단계",
+ "Previous": "이전",
+ "Editor mode is enforced!": "편집기 모드가 강제됐습니다!",
+ "Editor mode": "편집기 모드",
+ "Typewriter mode": "타자기 모드",
+ "information, Impressum, privacy policy": "정보, 관리자 정보, 사생활 정책",
+ "Preferences": "기본 설정",
+ "Game Info & Credits": "게임 정보 및 제작자 명단",
+ "Game Info": "게임 정보",
+ "Clear Progress": "진도 없애기",
+ "Erase": "지우기",
+ "Download Progress": "진도 내려받기",
+ "Download": "내려받기",
+ "Load Progress from JSON": "JSON에서 진도 불러오기",
+ "Upload": "업로드",
+ "Home": "홈",
+ "back to games selection": "게임 선택하러 돌아가기",
+ "close inventory": "인벤토리 닫기",
+ "show inventory": "인벤토리 보기",
+ "World": "세계",
+ "Show more help!": "도움말 더 보기!",
+ "Goal": "목표",
+ "Current Goal": "현재 목표",
+ "Objects": "객체",
+ "Assumptions": "가정",
+ "Further Goals": "이후 목표",
+ "No Goals": "목표 없음",
+ "Loading goal…": "목표 불러오는 중…",
+ "Click somewhere in the Lean file to enable the infoview.": "린 파일의 아무 곳이나 눌러 정보창을 여십시오.",
+ "Waiting for Lean server to start…": "린 서버가 시작하기를 기다리는 중…",
+ "Level completed! 🎉": "단계 완료! 🎉",
+ "Level completed with warnings 🎭": "경고 있는 채로 단계 완료 🎭",
+ "Active Goal": "활성화된 목표",
+ "Crashed! Go to editor mode and fix your proof! Last server response:": "시스템 다운됨! 편집기 모드에서 증명을 고치십시오! 마지막 서버 응답:",
+ "Line": "줄",
+ "Character": "문자",
+ "Loading messages…": "메시지 불러오는 중…",
+ "Execute": "실행하기",
+ "Definitions": "정의",
+ "Theorems": "정리",
+ "Not unlocked yet": "아직 잠금 해제가 안 됨",
+ "Not available in this level": "이 단계에서 쓸 수 없음",
+ "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "<1>린(Lean 4)<\/1> 증명 보조기와 그 수학 라이브러리 <5>매스리브(mathlib)<\/5>를 학습하기 위한 게임들의 저장소",
+ "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "불러온 게임 없음. <1>http:\/\/localhost:3000\/#\/g\/local\/FOLDER<\/1>를 이용해 지역[로컬] 폴더에서 게임을 직접 여십시오.",
+ "
As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.
<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "이 서버는 저희 대학의 여러 컴퓨터에서 린을 실행하므로 그 이용량이 제한돼 있습니다. 현재 이 서버로 최대 70게임을 동시에 실행할 수 있는 것으로 추정됩니다. 미래에 저희가 서버 이용량 한계에 더 잘 대처하고 그 값을 보다 정확히 측정할 수 있기를 바랍니다.<\/p><1>게임과 그 기반 시설의 상당 부분은 여전히 개발 중입니다. 문제를 겪으면 거리낌 없이 <1>깃허브 이슈<\/1>를 제출해 주세요!<\/1>",
+ "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "이 서버는 뒤셀도르프의 하인리히-하이네 대학에서 진행하는 <1>'아담(ADAM): 수학의 디지털 시대 준비하기'<\/1> 프로젝트의 일환으로 개발됐습니다.",
+ "Prerequisites": "선행 요건",
+ "Worlds": "세계",
+ "Levels": "단계",
+ "Language": "언어",
+ "Server capacity": "서버 이용량",
+ "RAM": "램",
+ "CPU": "CPU",
+ "used": "쓰임",
+ "Development notes": "개발 노트",
+ "Adding new games": "새 게임 추가하기",
+ "Funding": "재정 지원",
+ "
Do you want to delete your saved progress irreversibly?
(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)
": "저장된 진도를 불가역적으로 삭제하시겠습니까?<\/p>
(이를 선택하시면 증명과 인벤토리 안의 수집 항목들이 삭제됩니다. 다른 게임에 저장된 정보는 삭제되지 않습니다.)<\/p>",
+ "Delete Progress?": "진도를 삭제하시겠습니까?",
+ "Delete": "삭제하기",
+ "Download & Delete": "내려받고 삭제하기",
+ "Cancel": "취소하기",
+ "Layout": "레이아웃",
+ "Always visible": "항상 보임",
+ "Save my settings (in the browser store)": "(브라우저에) 설정 저장하기",
+ "
Select a JSON file with the saved game progress to load your progress.
<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "저장된 게임 진도가 있는 JSON 파일을 선택해 진도를 불러오십시오.<\/p><1><0>경고:<\/0> 이를 실행하면 현재의 게임 진도가 삭제됩니다! <2>현재의 게임 진도<\/2>를 먼저 내려받을지 판단하십시오!<\/1>",
+ "Upload Saved Progress": "저장된 진도 업로드",
+ "Load selected file": "선택한 파일 열기",
+ "Mobile": "모바일",
+ "Auto": "자동",
+ "Desktop": "데스크톱",
+ "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.
Featured games on this page are added manually. Please get in contact and we'll happily add yours.
": "<0>여러분이 직접 게임을 작성할 생각이 있다면, <1>GameSkeleton 깃허브 저장소<\/1>를 양식[템플릿]으로 이용하고 <3>'게임 만들기(Creating a Game)'<\/3> 문서를 읽으십시오.<\/0><1>여러분이 작성한 게임을 직접 서버에서 불러오고, 정확한 URL을 이용해 그 게임을 하실 수 있습니다. 여러분의 게임을 서버에서 불러오는 방법에 관한 세부 사항도 위의 <1>설명서<\/1>에 나와 있습니다. 궁금한 점이 있으면 저희에게 연락해 주십시오.<\/1>이 페이지에 실린 게임들은 수동으로 추가됐습니다. 저희에게 연락하시면 여러분의 게임을 기꺼이 추가하겠습니다.",
+ "Level": "단계",
+ "Introduction": "소개",
+ "Retry proof from here": "여기부터 증명 다시 시도하기",
+ "Retry": "다시 시도하기",
+ "Failed command": "실패한 명령"
+}
diff --git a/client/public/locales/ko/translation.json b/client/public/locales/ko/translation.json
new file mode 120000
index 0000000..ac9ecbf
--- /dev/null
+++ b/client/public/locales/ko/translation.json
@@ -0,0 +1 @@
+target/translation.json
\ No newline at end of file
diff --git a/client/public/locales/kr/translation.json b/client/public/locales/kr/translation.json
deleted file mode 100644
index 550cdde..0000000
--- a/client/public/locales/kr/translation.json
+++ /dev/null
@@ -1,94 +0,0 @@
-{
- "Intro": "",
- "Game Introduction": "",
- "World selection": "",
- "Start": "",
- "Inventory": "",
- "next level": "",
- "Next": "",
- "back to world selection": "",
- "Leave World": "",
- "previous level": "",
- "Previous": "",
- "Editor mode is enforced!": "",
- "Editor mode": "",
- "Typewriter mode": "",
- "information, Impressum, privacy policy": "",
- "Preferences": "",
- "Game Info & Credits": "",
- "Game Info": "",
- "Clear Progress": "",
- "Erase": "",
- "Download Progress": "",
- "Download": "",
- "Load Progress from JSON": "",
- "Upload": "",
- "Home": "",
- "back to games selection": "",
- "close inventory": "",
- "show inventory": "",
- "World": "",
- "Show more help!": "",
- "Goal": "",
- "Objects": "",
- "Assumptions": "",
- "Current Goal": "",
- "Further Goals": "",
- "No Goals": "",
- "Loading goal…": "",
- "Click somewhere in the Lean file to enable the infoview.": "",
- "Waiting for Lean server to start…": "",
- "Level completed! 🎉": "",
- "Level completed with warnings 🎭": "",
- "Failed command": "",
- "Retry proof from here": "",
- "Retry": "",
- "Active Goal": "",
- "Crashed! Go to editor mode and fix your proof! Last server response:": "",
- "Line": "",
- "Character": "",
- "Loading messages…": "",
- "Execute": "",
- "Tactics": "",
- "Definitions": "",
- "Theorems": "",
- "Not unlocked yet": "",
- "Not available in this level": "",
- "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "",
- "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "",
- "
As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.
<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "",
- "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.Featured games on this page are added manually. Please get in contact and we'll happily add yours.
": "",
- "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "",
- "Prerequisites": "",
- "Worlds": "",
- "Levels": "",
- "Language": "",
- "Lean Game Server": "",
- "Development notes": "",
- "Adding new games": "",
- "Funding": "",
- "Level": "",
- "Introduction": "",
- "Do you want to delete your saved progress irreversibly?
(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)
": "",
- "Delete Progress?": "",
- "Delete": "",
- "Download & Delete": "",
- "Cancel": "",
- "Mobile": "",
- "Auto": "",
- "Desktop": "",
- "Layout": "",
- "Always visible": "",
- "Save my settings (in the browser store)": "",
- "Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.
<1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp in a level, you can use it henceforth in any level.The options are:
": "",
- "Game Rules": "",
- "levels": "",
- "tactics": "",
- "regular": "",
- "relaxed": "",
- "none": "",
- "Select a JSON file with the saved game progress to load your progress.
<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "",
- "Upload Saved Progress": "",
- "Load selected file": "",
- "Rules": ""
-}
diff --git a/client/src/config.json b/client/src/config.json
index d6408ee..cc4261d 100644
--- a/client/src/config.json
+++ b/client/src/config.json
@@ -28,7 +28,7 @@
"name": "Español"
},
{
- "iso": "kr",
+ "iso": "ko",
"flag": "KR",
"name": "한국어"
}